practal

20 ms·

211.
by practal 4y ago
I just came across Yuri's criticism for the first time, but it makes sense to me. I am not a user of Julia, but have followed it with interest since they published their first paper about it. With hindsight, it is clear that they would
212.
by practal 4y ago
Yes, I will concede that of course PTS can be used in a "first the invariants, then the code" way, and so my distinction doesn't make much sense here. Nevertheless, PTS is for verifying imperative programs, and if whenever po
213.
by practal 4y ago
It's a weird example, but you definitely got a point. Of course, an ambiguity like in your example never causes a problem, because this text is parsed by humans, not by machines!
214.
by practal 4y ago
I've heard of nuPRL, it seems to be also based on type theory, with special emphasis on constructivity. It's basically the same as Coq, foundationally. At a summer school Bob Constable once said that he would refuse to fly in a pl
215.
by practal 4y ago
No worries, happy to talk about this stuff all day long! The links are in a higher up post, they are: [0] https://obua.com/publications/philosophy-of-abstraction-logi... [1] https://obua.com/publication
216.
by practal 4y ago
PTS and Hoare-logic are really the same, just differently formulated. At least according to Wikipedia: https://en.wikipedia.org/wiki/Predicate_transformer_semantic... What I mean by my comment is that typically with Ho
217.
by practal 4y ago
The topic of mathlib might be different, but the methods are the same. That's why you can use Lean for both in the first place!
218.
by practal 4y ago
See my other answers. Curry-Howard is interesting, but making it the foundation of theorem proving is a choice (in my opinion, not a very good one), not a necessity, as most Curry-Howard fans seem to think.
219.
by practal 4y ago
Automated verification is not the latest in a long list of fads. First, it is not a fad, and second, it has been around for a long time (check for example [0], which dates from 1961). I agree with you that constructing programs such that th
220.
by practal 4y ago
See my reply to you deeper below.
221.
by practal 4y ago
Interesting point. Let's say 1% of all mathematicians. That would be many.
222.
by practal 4y ago
I am aware of Lean and mathlib. It's the group around Kevin Buzzard which is doing mathlib, and it is for sure a great effort. Being practical, they latched onto the theorem proving facilities that are currently available, Lean certain
223.
by practal 4y ago
Citing your link: > At this point, however, you may be feeling that type theory sounds very complicated. Lots of different ways to form types, each with their own rules for forming elements? Where is the simplicity and intuitiveness that
224.
by practal 4y ago
Most mathematicians don't even use formal logic. For sure they don't use type theory! You seem to be the one who is silly/confused here. If you want to lift your confusion, read the [0] link I gave above.
225.
by practal 4y ago
Yes, and because of that limitation dependent type theory is an inferior logic for theorem proving.
226.
by practal 4y ago
Well, if you created a new data structure not known before, and proved theorems about it, that's new math. If you copied a well-known data structure, and prove theorems about it, that's not new math. What do you think mathematicia
227.
by practal 4y ago
First, theorem proving is NOT the same as an advanced form of static typing. This is a misunderstanding mostly pushed by computer scientists. Instead of propositions as types, I advocate a more practical form of types, based on Abstraction
228.
by practal 4y ago
Formal verification is just very costly and has diminishing returns. Let's take a CAD program. Which aspects of it would you formally verify? If you are going for the easy parts, those can already be dealt with nicely with static typin
229.
by practal 4y ago
There was a version of Lean that supported HoTT, and I think it helped in making Lean popular. But that support has been dropped in Lean 3, and Lean 4 does not support it either. Lean 4 itself seems to be a radical rewrite, and libraries wr
230.
by practal 4y ago
Not if you do software the right way. Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... Furthermore, I don't think cutting-edge math needs a much different approach from cutting-edge s
231.
by practal 4y ago
The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. A nice example is the recent formalisation in Lean of some ideas by Peter Scholze: https://
232.
by practal 4y ago
I am sure we can do better than predicate logic or types, but the code needs to change also. Code should be more abstract and reusable. If possible, it should be a subset of the logic. There is no point in verifying the same stuff in JavaSc
233.
by practal 4y ago
If you are more practical than religious, try this: https://functional-algorithms-verified.org
234.
by practal 4y ago
Thanks! But it is actually an old field by now, and there are quite a few conferences for it. Although automated theorem proving and interactive theorem proving have developed on different tracks, they are slowly converging in the last 15 y
235.
by practal 4y ago
Don't worry about it, I've showed it to the best people in the field (you would think), and haven't gotten much of a response out of most of them so far. It is a VERY conservative field. At least nobody so far said it's
236.
by practal 4y ago
When you create a new logic with certain applications in mind, it might be unsound at some intermediate steps, like you can have bugs in a program. But yeah, I don't think there is much use for an unsound logic per se.
237.
by practal 4y ago
> Unlike conventional theorem provers, Holbert’s term language is just the untyped lambda calculus. While this technically makes the logic unsound, it is much simpler to use as a pedagogical tool. I am not sure if it is very pedagogical
238.
by practal 4y ago
This makes a lot of sense. I have been working on something similar, along the lines of mixing Latex and Markdown, and christened it "Recursive TeXt". Currently it only exists as a macOS app with me as the only user (it is still e
239.
by practal 4y ago
We share this objective! I am sharing my thoughts on that here: https://practal.com
240.
by practal 4y ago
No. Constructive analysis is not needed for this. Classical mathematics will do just fine. Stating nonsense like this is what gives constructivism a bad name. That's not saying that there is no room for constructivism in an ideal ITP&#

More ›