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

141–150 of 203 posts

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

#141

Post by practal »

ebingdom wrote: post #136
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…

> 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 math is really a subset of what's needed for software. That is obvious to me, but I don't have a citation. You can cite me, if you want to.

Finally, dependent types as it is done today in Coq and Lean etc. is not nice enough a logic to attract mathematicians. The reason for that is that it is not nice enough a logic, full stop. So why would it be nice enough for computer scientists? Oh, because your problems are simpler, so you don't need a nice logic?

Saying that Martin-Löf type theory can do arbitrarily fancy math is both false and right. Just as saying that anything can be programmed in assembler is both false and right. Yeah, with enough focus and discipline you probably can, but who would want to?

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

#142

Post by renox »

marcosdumay wrote: post #23
daenz wrote: post #6

Outside of mission critical applications, if the cost involved to make software "provably correct" (time, salaries) is greater than the cost of the bugs, it will never be adopted. Believe me, I see the appeal, but it's kind of like demanding your house have all perfect right angles and completely level surfaces. Living with manageable imperfection is far more realistic.

We use static type systems all the time, as well as specialized checkers and linters, and none of those showed themselves to have "costs greater than the cost of the bugs". And none of them are even nearly similar to "demanding your house have all perfect right angles and completely level surfaces". Do you have any reason to believe that all the rest of the verification theory is completely impractical when every pie…

Using a language with provides static typed != using static types, quite a few programs bypass the static types with 'everything is an int' or 'everything is a string'..

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

#143

Post by guerrilla »

ebingdom wrote: post #102
guerrilla wrote: post #45

Earlier quoted context omitted.

> First get mathematicians to actually like doing proofs with the help of a computer. Many are using type theoretic and HOL theorem proves already. What threshold do we need to reach? Isn't Lean HoTT? Isn't that pretty much good enough (modulo UI and tooling)? I ask the latter question because that was the original promise of HoTT but I haven't kept up to date on Lean, so I'm asking.

> Isn't Lean HoTT? No. Lean is good old fashioned Martin-Löf type theory. HoTT is that type theory + univalence + higher inductive types. Lean actually has proof irrelevance, which is incompatible with HoTT. But the good news is you don't need HoTT to verify software. Type theory is already quite capable of it, despite what others in this thread would like you to believe.

> Type theory is already quite capable of it, despite what others in this thread would like you to believe.

I know but mathemeticians wanted HoTT.

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

#144

Post by guerrilla »

practal wrote: post #134
ebingdom wrote: post #130

Earlier quoted context omitted.

> Let's take a CAD program. Which aspects of it would you formally verify? Any large program will contain some smaller components with relatively well-defined behavior. CAD is not my specialty, so I can't really comment on what algorithms are used in that domain. Forgetting about fancy algorithms for a moment, just having a more expressive type system will allow you to express invariants in your code like the fact th…

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…

> First, theorem proving is NOT the same as an advanced form of static typing.

Yes it very much is in a dependent type theory.

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

#145

Post by guerrilla »

practal wrote: post #92
guerrilla wrote: post #45

Earlier quoted context omitted.

> First get mathematicians to actually like doing proofs with the help of a computer. Many are using type theoretic and HOL theorem proves already. What threshold do we need to reach? Isn't Lean HoTT? Isn't that pretty much good enough (modulo UI and tooling)? I ask the latter question because that was the original promise of HoTT but I haven't kept up to date on Lean, so I'm asking.

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.

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

#146

Post by [deleted] »

Hizonner wrote: post #64
AlotOfReading wrote: post #31

I really want to like this, but it really comes across as more of a wishful thinking project without a lot of experience or intuition about how to solve the very real problems that formal methods run into in this domain. Like, the design goals literally include "verify any program" [1], which is almost certainly impossible. Important questions like how you implement the design pillars without running smack into the i…

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…

[deleted]

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

#147

Post by practal »

guerrilla wrote: post #144
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…

> First, theorem proving is NOT the same as an advanced form of static typing. Yes it very much is in a dependent type theory.

Yes, and because of that limitation dependent type theory is an inferior logic for theorem proving.

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

#148

Post by ebingdom »

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…

> The reason for that is that it is not nice enough a logic, full stop. So why would it be nice enough for computer scientists?

Type theory has many attractive properties over traditional foundations like set theory. See, for example: https://golem.ph.utexas.edu/category/2013/01/from_set_theory...

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

#149

Post by [deleted] »

muglug wrote: post #17

This builds on the success of Rust, but Rust has not been a success when it comes to [number of engineers writing professional code in the language]. By that measure it's still incredibly niche compared to interpreted languages. The main reason why formal verification has not had even the success of Rust is that most developers (myself included) don't know enough about the area to take an interest, and certainly don'…

[deleted]

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

#150

Post by guerrilla »

practal wrote: post #147
guerrilla wrote: post #144

Earlier quoted context omitted.

> First, theorem proving is NOT the same as an advanced form of static typing. Yes it very much is in a dependent type theory.

Yes, and because of that limitation dependent type theory is an inferior logic for theorem proving.

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.

Post reply on HN