Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Make formal verification and provably correct software practical and mainstream

github.com

Post reply on HN
Print view View original

171–180 of 203 posts

Re: Make formal verification and provably correct software practical and mainstream

#171

Post by mbrodersen »

practal wrote: post #141
ebingdom wrote: post #136

Earlier quoted context omitted.

> First, theorem proving is NOT the same as an advanced form of static typing. This Hacker News post is about a theorem prover based on dependent types. That's the context for our discussion. > You will still have buggy programs in which you use those components No one is disagreeing with this claim. But eliminating some bugs is better than nothing, even if you don't eliminate all bugs. You and the other commenters r…

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 mathematicians do? They just examine certain things rigorously and with utmost scrutiny. These things are simpler than things appearing in real-life. Software interfaces with real-life, so cutting-edge…

Professional mathematicians are today using dependent types in LEAN to prove leading edge mathematics. Google LEAN and mathlib.

Re: Make formal verification and provably correct software practical and mainstream

#172

Post by [deleted] »

practal wrote: post #151
guerrilla wrote: post #150

Earlier quoted context omitted.

That's silly. Whether it's a good or bad metatheory for theorem proving depends entirely on one's goals and preferences. Most mathematicians use a type theory over something else, so it's hard to even take your view seriously. On top of that, you seem very opinionated for someone who was just confused about the topic of this thread. I have no idea why you're waging a holy war over this but maybe take a break.

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.

[deleted]

Re: Make formal verification and provably correct software practical and mainstream

#173

Post by Tainnor »

_vdpp wrote: post #66
Hizonner wrote: post #64

Earlier quoted context omitted.

I agree it sounds like pretty naive enthusiasm. Not just about how hard the formal verification problem is, but about how hard it is to get ANY kind of programming system up to the point where it's actually usable. However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are…

A lot of people take undecidability to mean “no program can be proven to terminate” when in reality it means “there exist programs which are impossible to prove termination,” and like you said most of the useful programs we write can be shown to terminate just fine.

I agree in general and also take issue with the "we can never prove interesting things about our programs" statements that are sometimes uttered, but it is surprisingly easy to write certain programs that nobody to this date knows whether they terminate, such as: "find the least even number > 2 that cannot be written as the sum of two primes". :)

Re: Make formal verification and provably correct software practical and mainstream

#174

Post by practal »

mbrodersen wrote: post #171
practal wrote: post #141

Earlier quoted context omitted.

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 mathematicians do? They just examine certain things rigorously and with utmost scrutiny. These things are simpler than things appearing in real-life. Software interfaces with real-life, so cutting-edge…

Professional mathematicians are today using dependent types in LEAN to prove leading edge mathematics. Google LEAN and mathlib.

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 certainly being one of the best at this moment. But just because they can make type theory work for them, with much effort, doesn't mean that it is the right way to do formal math. They are still a drop in the ocean compared to all the mathematicians who have never touched a proof assistant. I find it telling that in the Liquid Tensor experiment Peter Scholze didn't touch Lean himself, but worked through this group as intermediaries, who mediated the type theory details for him.

The state of proof assistants is such that currently almost all of them are based on some form of type theory. There are exceptions like Mizar and Metamath (Zero), which are based on first-order logic. Type theory seemed to be the only way to have proper general variable binding, via lambdas, and that is the main reason for its popularity today. Type theory is a particular mathematical theory, though, and not particularly well suited to most things mathematicians like to do, like forming completions or subsets of types/sets. Type theory also cannot deal with undefinedness properly. Of course, there are methods of working around these issues like coercions and option types, but they are cumbersome.

Until recently I also thought that a minimum of type theory is necessary, to get general variable binding. For example, I tried to embed set theory within simply-typed higher-order logic ([2]).

But since last year I know that you don't need type theory for variable binding (see [0])! Of course, (dependent) types are still useful, but now you can work with them in a much more flexible way, without having to divide the mathematical universe into separate STATIC and A PRIORI chunks labelled by types (see [1], but that needs to be updated with the understanding gained from [0]).

If type theory works for you, fine. But I know there is a better way.

[2] https://link.springer.com/chapter/10.1007/978-3-319-20615-8_...

Re: Make formal verification and provably correct software practical and mainstream

#175

Post by Thiez »

nottorp wrote: post #121

You can prove that an algorithm is correct most of the time (yes, halting and decidability but for practical purposes you mostly can). How do you prove an event driven application is correct?

Modelling your application as a state machine will allow you to use model checking to prove various properties about your model. Proving that your program is equivalent (for some chosen definition of equivalence) to the state machine is left as an exercise for the reader.

Re: Make formal verification and provably correct software practical and mainstream

#176

Post by practal »

guerrilla wrote: post #145
practal wrote: post #92

Earlier quoted context omitted.

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://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... That's great stuff, which shows what can in principle be done with this technology. But why is a team necessary to formalise Scholze's…

> The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. No, you didn't answer the question at all. How many is many? How many will be enough for you? It is being used by mathematicians and for some pretty important things.

Interesting point. Let's say 1% of all mathematicians. That would be many.

Re: Make formal verification and provably correct software practical and mainstream

#177

Post by practal »

mbrodersen wrote: post #168
practal wrote: post #30

Earlier quoted context omitted.

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 JavaScript, Java, Rust, Swift, ... Furthermore, something that looks simple might need a lot of abstraction to become provable. Something might be simple to write down in code, but in or…

Mathematicians are using LEAN today to prove learning edge mathematics correct. Google LEAN and mathlib.

See my reply to you deeper below.

Re: Make formal verification and provably correct software practical and mainstream

#178

Post by practal »

User23 wrote: post #161
practal wrote: post #30

Earlier quoted context omitted.

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 JavaScript, Java, Rust, Swift, ... Furthermore, something that looks simple might need a lot of abstraction to become provable. Something might be simple to write down in code, but in or…

Verification is largely a fool's errand[1]. The juicy opportunity is tooling that aids in constructing programs such that they necessarily have the desired properties. Predicate transformer semantics are up to the task. It's basically just applied lattice theory, which is a very well understood field of math and within the learning capacity of any competent programmer. Edit: Automated verification does however attrac…

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 they necessarily have the desired properties is the way to go. But we will disagree in how to go about that. Predicate transformer semantics is just another name for Hoare-Logic, and is too narrowly focused on the program code itself. It is basically the opposite of correct by construction! Rather, I would like to see programs as natural outflows / consequences of verified mathematical theories.

[0] https://en.wikipedia.org/wiki/DPLL_algorithm

Re: Make formal verification and provably correct software practical and mainstream

#179

Post by practal »

mbrodersen wrote: post #170
practal wrote: post #134

Earlier quoted context omitted.

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 Logic [0, 1]. Second, yes of course, you can carve out components and concentrate on those. If you can find opportunities for this, great! You will still have buggy programs in whi…

It literally is. Martin Luff Type Theory is the mathematical foundation used by most proof assistants today . The type checker is the prover. If your code type checks then you have proven a theory. I highly recommend learning more about the Curry Howard correspondence and Dependent Types. It might just blow your mind.

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.

Re: Make formal verification and provably correct software practical and mainstream

#180

Post by practal »

mbrodersen wrote: post #169
practal wrote: post #118

Earlier quoted context omitted.

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 software. You need to be able to express your thoughts succinctly, and have the tools to reason about them. It is often said that software verification is different because there is much…

All of those problems can be proven correct today using Coq/HOL/LEAN etc. see CompCert, seL4 etc. The math needed by Computer Scientists to prove correct is very different from what Mathematicians care about. Look at the mathlib project done by mathematicians in LEAN. It is pretty much useless if you want to prove code correct.

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!
Post reply on HN