Make formal verification and provably correct software practical and mainstream • Hacker News Board

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

#161

Post by User23 » Sun, May 29, 2022, 7:20 PM UTC

practal wrote: post #30

Animats wrote: post #20

"And all existing proof languages are hopelessly mired in the obtuse and unapproachable fog of research debt created by the culture of academia." Yes. As I wrote 40 years ago: "There has been a certain mystique associated with verification. Verification is often viewed as either an academic curiosity or as a subject incomprehensible by mere programmers. It is neither. Verification is not easy, but then, neither is wr…

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 attract a lot of research money as the latest in a long list of fads promising the bean counters that they can hire cheap idiot programmers instead of expensive smart ones. I don't mean to be dismissive though, the automatic verification research is genuinely interesting and they have accomplished impressive things, for example[1].

[1] https://www.semanticscholar.org/paper/Learning-Loop-Invarian...

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

#162

Post by drc500free » Sun, May 29, 2022, 7:24 PM UTC

pron wrote: post #138

Wow, the language here is even more optimisitc than the rosiest descriptions you see from young researchers, which prompted me to check if the author has had much experience deductively verifying interesting "deep" functional properties of non-trivial programs. The answer seems to be no. Like a newcomer to the field, he focuses on "first-day" problems such as language convenience, but the answer to his question of wh…

> Another problem is an incorrect model of how programs are constructed. One might think that if a programmer has written a program, then they must have some informal (but deductive) model of it in their mind, and all that's missing is "just" formally specifying it. But that is not how programs are constructed over time when many people are involved.

And that's just looking at how things work within the engineering teams. What is the perfect software for "we need an identity card system for physical and logical authorization of two million military personnel"?

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

#163

Post by shoo » Sun, May 29, 2022, 9:28 PM UTC

chmod600 wrote: post #110

shoo wrote: post #18

Earlier quoted context omitted.

Exactly. In many settings it is quite a reasonable business decision to regard a bug as WONTFIX. Here's one example: developer: adding proposed feature A to API B may result in displaying inconsistent data to the customer, in this kind of situation team owning service of API B, some weeks later: thank you for flagging that. we have thought about this, and propose a slightly different API design B'. let's meet to disc…

Defects, and potential defects, tend to cause a background of mental overhead, and communication overhead, throughout the organization. People have to remember what kinds of assumptions are broken under what circumstances, and relate that to a business impact. There's a mental unburdening when you can just say "situation X won't happen".

great point, the more of these kinds of shortcuts accumulate, the more complicated it becomes to think about related changes in future, making maintenance, training new team members more time consuming and expensive. maybe not quite the same as "technical debt", but some kind of debt.

tangentially, re: organising things to reduce cognitive load, there is an interesting discussion with the authors of the book "team topologies" who characterise the purpose of platform teams as existing to _reduce the cognitive load of stream-aligned teams_ (who have the goal of providing a user-facing service or product, say). https://www.infoq.com/podcasts/software-architecture-team-to...

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

#164

Post by UncleMeat » Sun, May 29, 2022, 10:59 PM UTC

abeyer wrote: post #159

UncleMeat wrote: post #154

Earlier quoted context omitted.

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.

Passing an object by reference to a function creates an alias. Storing a pointer as a field creates an alias. It would be very odd to have a program with zero aliasing relationships. Do do this you would need to never assign from a pointer type.

This has nothing to do with C (mostly - you havoc more frequently when analyzing C if you want to be sound). Pointer Analysis papers usually target Java and in that space it is still stunningly difficult.

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

#165

Post by mbrodersen » Mon, May 30, 2022, 2:07 AM UTC

akomtu wrote: post #53

I suspect that verifying software is a lot like the termination problem of Turing machines: the more useful properties you want to verify, the closer it is to NP completeness. So a practical verifier should limit its scope to a modest subset of software and settle on verifying sonething with a sufficient degree of confidence, which is lower than 100%.

It turns out that you can write proven correct C compilers (CompCert), proven correct Operating Systems (seL4), and proven correct secure network protocols using proof assistants like Coq and F*. All of those proof assistants are using languages that are not Turing complete. You have to prove termination if the proof assistants can’t automatically prove it. So being Turing complete is not really necessary for writing complex software.

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

#166

Post by mbrodersen » Mon, May 30, 2022, 2:12 AM UTC

warkdarrior wrote: post #62

akomtu wrote: post #53

I suspect that verifying software is a lot like the termination problem of Turing machines: the more useful properties you want to verify, the closer it is to NP completeness. So a practical verifier should limit its scope to a modest subset of software and settle on verifying sonething with a sufficient degree of confidence, which is lower than 100%.

Both termination and verification go beyond NP completess, in that they are undecidable. Also, "verifying so[m]ething with... confidence... lower than 100%" is known as testing.

Termination is undecidable in general but that is not a problem in practice. Proof assistants like Coq, LEAN etc. can automatically prove termination for most practical code. And if not, the developer has to prove termination by hand. Which is not hard in most cases I have encountered. And if you still can’t do it you simply add a “fuel” natural number counter that guarantees termination (exit when out of fuel).

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

#167

Post by deterministic » Mon, May 30, 2022, 2:16 AM UTC

agentultra wrote: post #58

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 is wishful thinking. Iris is cool and all but extracting useful programs from proofs is still an open research area. I don’t want to discourage someone from trying but it would help to be pragmatic. At least the author seems somewhat aware of this when they describe the repo as a collection of earnings and ravings. I’ve been interested in this since 2015 or so and even then the cost of doing formal verification ha…

Not at all. See CompCert, seL4, F* (F-star) and Coq for examples of how it is done.

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

#168

Post by mbrodersen » Mon, May 30, 2022, 2:18 AM UTC

practal wrote: post #30

Animats wrote: post #20

"And all existing proof languages are hopelessly mired in the obtuse and unapproachable fog of research debt created by the culture of academia." Yes. As I wrote 40 years ago: "There has been a certain mystique associated with verification. Verification is often viewed as either an academic curiosity or as a subject incomprehensible by mere programmers. It is neither. Verification is not easy, but then, neither is wr…

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.

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

#169

Post by mbrodersen » Mon, May 30, 2022, 2:21 AM UTC

practal wrote: post #118

ebingdom wrote: post #114

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. The kinds of theorems that we need to prove in software are much more elementary than what mathematicians are proving. I think software engineering can benefit from it long before mathematicians start doing cutting-edge math in it.

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.

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

#170

Post by mbrodersen » Mon, May 30, 2022, 2:24 AM UTC

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…

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.