6 ms·

I used to do proof of correctness work, decades ago.[1] We had more proof automation than many of the later systems. The easy stuff was solved by the first SAT

by Animats 4mo ago

I used to do proof of correctness work, decades ago.[1] We had more proof automation than many of the later systems. The easy stuff was solved by the first SAT solver, the Oppen-Nelson simplifier. The harder stuff used the Boyer-Moore prover, which uses heuristics and previous lemmas to guide the theorem prover. The Boyer-Moore prover had to be helped along by suggesting lemmas, which it would try to prove and which would then be used for later proofs. That was the tough human job. Later systems seemed to have less automation. What tended to go wrong with formal methods was that the people doing them were too into the formalism. I was working on this for a commercial project that wanted bug-free code, not as an academic. The academic projects tended to get too clever. They had the mathematician's bias of wanting a terse notation and not much case analysis. That's not a good solution. You want lots of automated grinding and don't want to need much insight. The clever people kept inventing new logics - modal logic, temporal logic, etc, - to avoid verbosity in paper and pencil proof work. That wasn't really all that helpful. The basic truth of this business is that most of the theorems are rather banal. As the Jane Street people point out, there's a big advantage in having control of the language. You want the verification statements integrated into the programming language. In many systems, they're embedded in comments, in a different syntax than the programming language, or even in completely separate files. This adds unnecessary work. It's good to see them pushing this forward. We were doing this too early, over 40 years ago. It took about 45 minutes of compute back then to build up number theory from a cold start with the Boyer-Moore prover. Now it takes less than a second. [1] https://archive.org/details/manualzilla-id-5928072/page/n3/mode/2up https://archive.org/details/manualzilla-id-5928072/page/n3/m...

nextos 4mo ago
I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like LTL or, more recently, separation logic, have been incredible breakthroughs. TLA+, which has gained quite a lot of popularity, is a testament to that. Model checking is eminently practical. The exciting thing now is that heavier formal methods, in particular theorem proving, might become cheap enough to use in regular systems software. Writing formal specifications for functions and getting them synthesized and proven correct by some SAT/SMT, theorem prover & LLM hybrid may become the norm in the not-too-distant future. [1] On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf [2] From Philosophical to Industrial Logics. https://www.cs.rice.edu/~vardi/papers/icla09.pdf https://www.cs.rice.edu/~vardi/papers/icla09.pdf
- arka2147483647 4mo ago
  > Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. It sounds like what you think as positives are exactly the things parent comment thinks as negatives.
  - ajb 4mo ago
    There's a big difference between wanting a succinct proof and wanting a succinct statement of the requirements. The easier it is to state the requirements, the more likely you have stated them correctly. Whereas succinct proof is not relevant for industrial purposes, as long as the proover has a small trusted kernel, it makes no difference to the reliability.
  - agentcoops 4mo ago
    I used to work in this field myself long ago (academically and practically). The difficulty that OP didn't suggest much appreciation for is that the interesting spaces for automated verification -- especially of distributed systems, say -- require exploring the space of formalisms between the trivial proofs of propositional logic (SAT solvers) and the undecidable proofs of first or second-order logic (interactive theorem proving environments such as Isabelle and Lean). This is the incredibly large space occupied most importantly by the various modal logics, which allow for quantification over graph traversals. There are remarkably expressive logics where the decision problem remains tractable, such as the modal mu-calculus. That is, precisely if one wants automated tools for verification the seemingly obtuse work on novel formal systems is necessary.
- jmalicki 4mo ago
  "Logic is to computer science and software engineering what calculus is to ... mechanical or civil engineering" Things professionals rarely use in practice?
- YetAnotherNick 4mo ago
  > TLA+, which has gained quite a lot of popularity Why do you think that? Outside of just toy examples, and vague examples of "AWS uses that", I don't know of any actual code which has TLA. Most of the things you can do with TLA, you can do with informal math notation quite easily. Do you have any real world long term usage examples?
ebiederm 4mo ago
Have you looked at ADA Spark? If you have does it match your intuition of how things should be done? I am slowly working on something where I hope to integrate such a capability for the things that type systems can't handle quickly. So I would be interested in perspectives of people who have been down this route before.
- Animats 4mo ago
  I've generally liked classic approaches which had entry and exit conditions, and loop invariants, all written using the same syntax and operators as the program. The compiler has to know what to ignore, of course. The compiler should syntax and type check all the proof information, even if it can't verify it. It's important to avoid an impedance mismatch between the proof system and the programming language. If programmers are constantly translating between two notations, customer resistance will be high. If you need to write functions as scaffolding for proofs, they should be written in the programming language. You might need some operators that aren't actually runnable, such as FORALL, but the syntax should be that of the programming language. If your specs look like Γ, P || Q, P ==> R, Q ==> R ⊢ R in a language with none of those operators, you're doing it wrong. That's the disease of falling in love with the formalism. The user should not have to tell the proof system things the compiler already knows. Whatever overloading and aliasing rules the language enforces should be known and handled in verification, too. We worked off the syntax tree produced by a compiler front end modified to handle the verification statements, not the raw source code. Ada Spark has different aliasing rules than Ada, for example. One big problem is that object oriented programming came and went in popularity. You really want object invariants. You need some way to attach an invariant to a data structure. You also need a clear boundary where control enters and exits the objects. If the language doesn't have objects, you struggle with trying to express object type invariants in the proof language. You don't get the boundaries as part of the programming language. A useful interface between the prover and the program is simply to use assert(A); assert(B); in the middle of code to encapsulate complex proof goals. A should be provable from the preceding code using a SAT solver. B, when assumed true, should provide enough info for a SAT solver to proceed from that point. Now you need to prove A implies B by external means. That creates a well defined problem which can be given to something AI-like, backed by a proof checker, to chew on. Ada Spark has some features that violate these rules. Also, it's hard to find anything about Ada Spark newer than ten years old. There's a fair amount of interest in verifying Rust. There's been some progress using Dafny. But "Dafny is not Rust. Using Dafny requires porting algorithms of interest from Rust to Dafny. This port can miss details and introduce errors." There's the impedance mismatch again. Verus looks more promising. It is more Rust-like in syntax, they get the SAT solver/AI prover distinction, and there's active development.
sgt101 4mo ago
Human interpretebility and human construction is going to be really important for formal specifications. My fear is that we will get inscrutable maths that will be guarded by tiny coteries of devoties. The different inscrutable notations will be mutually incompatible, understanding one will not really help with the others. Most people will simply write english statements that cannot be verified properly. Worse even, people will get machines to formalise their statements, and will not understand the formalism or the proofs, but will take part in the theatre of verification and act shocked when everything explodes.

by Animats 4mo ago

nextos 4mo ago

I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like LTL or, more recently, separation logic, have been incredible breakthroughs. TLA+, which has gained quite a lot of popularity, is a testament to that. Model checking is eminently practical. The exciting thing now is that heavier formal methods, in particular theorem proving, might become cheap enough to use in regular systems software. Writing formal specifications for functions and getting them synthesized and proven correct by some SAT/SMT, theorem prover & LLM hybrid may become the norm in the not-too-distant future. [1] On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf [2] From Philosophical to Industrial Logics. https://www.cs.rice.edu/~vardi/papers/icla09.pdf https://www.cs.rice.edu/~vardi/papers/icla09.pdf

arka2147483647 4mo ago
> Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. It sounds like what you think as positives are exactly the things parent comment thinks as negatives.
- ajb 4mo ago
  There's a big difference between wanting a succinct proof and wanting a succinct statement of the requirements. The easier it is to state the requirements, the more likely you have stated them correctly. Whereas succinct proof is not relevant for industrial purposes, as long as the proover has a small trusted kernel, it makes no difference to the reliability.
- agentcoops 4mo ago
  I used to work in this field myself long ago (academically and practically). The difficulty that OP didn't suggest much appreciation for is that the interesting spaces for automated verification -- especially of distributed systems, say -- require exploring the space of formalisms between the trivial proofs of propositional logic (SAT solvers) and the undecidable proofs of first or second-order logic (interactive theorem proving environments such as Isabelle and Lean). This is the incredibly large space occupied most importantly by the various modal logics, which allow for quantification over graph traversals. There are remarkably expressive logics where the decision problem remains tractable, such as the modal mu-calculus. That is, precisely if one wants automated tools for verification the seemingly obtuse work on novel formal systems is necessary.
jmalicki 4mo ago
"Logic is to computer science and software engineering what calculus is to ... mechanical or civil engineering" Things professionals rarely use in practice?
YetAnotherNick 4mo ago
> TLA+, which has gained quite a lot of popularity Why do you think that? Outside of just toy examples, and vague examples of "AWS uses that", I don't know of any actual code which has TLA. Most of the things you can do with TLA, you can do with informal math notation quite easily. Do you have any real world long term usage examples?

ebiederm 4mo ago

Have you looked at ADA Spark? If you have does it match your intuition of how things should be done? I am slowly working on something where I hope to integrate such a capability for the things that type systems can't handle quickly. So I would be interested in perspectives of people who have been down this route before.

Animats 4mo ago
I've generally liked classic approaches which had entry and exit conditions, and loop invariants, all written using the same syntax and operators as the program. The compiler has to know what to ignore, of course. The compiler should syntax and type check all the proof information, even if it can't verify it. It's important to avoid an impedance mismatch between the proof system and the programming language. If programmers are constantly translating between two notations, customer resistance will be high. If you need to write functions as scaffolding for proofs, they should be written in the programming language. You might need some operators that aren't actually runnable, such as FORALL, but the syntax should be that of the programming language. If your specs look like Γ, P || Q, P ==> R, Q ==> R ⊢ R in a language with none of those operators, you're doing it wrong. That's the disease of falling in love with the formalism. The user should not have to tell the proof system things the compiler already knows. Whatever overloading and aliasing rules the language enforces should be known and handled in verification, too. We worked off the syntax tree produced by a compiler front end modified to handle the verification statements, not the raw source code. Ada Spark has different aliasing rules than Ada, for example. One big problem is that object oriented programming came and went in popularity. You really want object invariants. You need some way to attach an invariant to a data structure. You also need a clear boundary where control enters and exits the objects. If the language doesn't have objects, you struggle with trying to express object type invariants in the proof language. You don't get the boundaries as part of the programming language. A useful interface between the prover and the program is simply to use assert(A); assert(B); in the middle of code to encapsulate complex proof goals. A should be provable from the preceding code using a SAT solver. B, when assumed true, should provide enough info for a SAT solver to proceed from that point. Now you need to prove A implies B by external means. That creates a well defined problem which can be given to something AI-like, backed by a proof checker, to chew on. Ada Spark has some features that violate these rules. Also, it's hard to find anything about Ada Spark newer than ten years old. There's a fair amount of interest in verifying Rust. There's been some progress using Dafny. But "Dafny is not Rust. Using Dafny requires porting algorithms of interest from Rust to Dafny. This port can miss details and introduce errors." There's the impedance mismatch again. Verus looks more promising. It is more Rust-like in syntax, they get the SAT solver/AI prover distinction, and there's active development.

sgt101 4mo ago

Human interpretebility and human construction is going to be really important for formal specifications. My fear is that we will get inscrutable maths that will be guarded by tiny coteries of devoties. The different inscrutable notations will be mutually incompatible, understanding one will not really help with the others. Most people will simply write english statements that cannot be verified properly. Worse even, people will get machines to formalise their statements, and will not understand the formalism or the proofs, but will take part in the theatre of verification and act shocked when everything explodes.