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

151–160 of 203 posts

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

#151

Post by practal »

guerrilla wrote: post #150
practal wrote: post #147

Earlier quoted context omitted.

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.

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.

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

#152

Post by practal »

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

> 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...

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 we expect of a foundational theory?

It's just not there, Mike. Type theory is neither simple nor intuitive, and it doesn't make a good foundation.

Type theory certainly has advantages, but it gets lost in esoteric texts like Mike's. There are two simple advantages over set theory within first-order logic: general variable binding, and that things are kept separate, for example that a boolean is not a number. Now, how to do general variable binding without static types I show in [0]. How to still keep things separate, in [1]. All without having to divide the mathematical universe into static types.

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

#153

Post by petergeoghegan »

Hizonner wrote: post #140
petergeoghegan wrote: post #65

Earlier quoted context omitted.

> One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this. "Industry programmers" are pretty far from being a monolith. There are a myriad of different approaches to testing, many of which are domain specific, for all kinds of reasons. Usually the way that a new testing tool gets adapted is that individual programmers or companies that adapt…

Because many of the costs of their irresponsible practices are externalized.

> Because many of the costs of their irresponsible practices are externalized.

I'm sure that that's true in at least some important cases. I don't see what it has to do with formal verification.

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

#154

Post by UncleMeat »

praptak wrote: post #89
AlotOfReading wrote: post #69

Earlier quoted context omitted.

I disagree that most interesting programs don't need things that are Hard to Verify. For instance, approximately every C program would benefit from correct pointer analysis, yet this remains an open research question. For a personal example, I had a recent lunch interaction with our security team about some work I wanted to do formally verifying bits of a bootloader we have. Halfway through the conversation, one of t…

> approximately every C program would benefit from correct pointer analysis, yet this remains an open research question. To me this falls under "you don't understand the code enough to want to use it". Which in case of unsafe pointers is a well established conclusion. In the C-land even well vetted security-related code keeps on delivering pointer bugs.

Pointer analysis is not just about lifetimes. It asks questions like “can these two names alias?, must these two names alias?, what objects can this name point to?”

This is considerably harder than ownership analysis.

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

#155

Post by abeyer »

AlotOfReading wrote: post #83
abeyer wrote: post #77

Earlier quoted context omitted.

Sure, but how many of those C programs are inherently hard to verify vs how many of them are hard because they happen to be built with tools that make them hard to verify?

I don't think those are fully separable concepts in legacy, spaghetti code. Regardless, I agree that if you're willing to architect your system around the need to formally verify it, the problem is somewhat tractable and getting more so every year as tools improve. Non-experts still might need the occasional "justifiable shortcut" instead of proving everything, but it's doable.

Sure, I don't think anyone is realistically expecting to verify all existing legacy spaghetti code -- _that's_ an interesting research direction, at best.

The point upthread (at least the point I took) is not that existing code doesn't do things to make it difficult to verify, but rather there's no reason inherent to the desired behavior of those programs that it _needs_ to be difficult to verify them. Nor is there good reason going forward to not lean towards tools that make verification more tractable for anything new we write.

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

#157

Post by drc500free »

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…

It gives me the same feeling as crypto-contracts. Someone with a very narrow range of low-level experience arm-chairs their way into a solution for a problem. That problem isn't even the hard problem for the domain, but they've thought a lot about it in a vacuum.

What is the "verifiability" of an e-commerce funnel? Of a recommendation engine? Of a national identity card system?

It doesn't take a lot of real-world experience to recognize that the specification process is generally more error-prone and imprecise than the coding process, but it does take some.

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

#158

Post by User23 »

_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.

We have general methods for constructing programs that have some desired property, such as termination.

We have no general methods for finding whether or not some arbitrary program has some desired property, such as termination.

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

#159

Post by abeyer »

UncleMeat wrote: post #154
praptak wrote: post #89

Earlier quoted context omitted.

> approximately every C program would benefit from correct pointer analysis, yet this remains an open research question. To me this falls under "you don't understand the code enough to want to use it". Which in case of unsafe pointers is a well established conclusion. In the C-land even well vetted security-related code keeps on delivering pointer bugs.

Pointer analysis is not just about lifetimes. It asks questions like “can these two names alias?, must these two names alias?, what objects can this name point to?” This is considerably harder than ownership analysis.

Ok, which of those programs can _only_ be implemented via aliasable pointers?

I don't think anyone is arguing that C's loose memory model and rampant undefined behavior are amenable to verification. The point is that neither of those are necessary in many of the places they've been used.

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

#160

Post by User23 »

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…

Most mathematicians are doing work that is, frankly, formally unsound. There's a huge culture of hidden assumptions in most mathematical fields.

Not to mention that the syntax is literally unparseable. For example what does this mean?

  sin(x) + cos(x)
Most mathematicians would say it's the sum of the sine of x and the cosine of x. But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o, and s(x). Obviously that kind of ambiguity is unacceptable in a formal procedure syntax like that used by programming languages. That's just a simple example, traditional math is full of this kind of thing.
Post reply on HN