> 36. The use of a program to prove the 4 color theorem will not change mathematics -- it merely demonstrates the theorem, a challenge for a century, is probably not important to mathematicians.
For the sake of completeness, the Four Colour Theorem was proved with the aid of a computer in 1976, although there were, er, quibbles with the original published result not finally put to bed until 1989. It was the first major theorem to be proved with computer assistance (Appel and Haken broke the theorem down to ~1400 configurations that were all computer verified).
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.
Rust proc macros are good enough to have design-by-contract implemented in them, although for type invariants it's not exactly ergonomic (because you have to disallow inner mutability to avoid someone grabbing a reference to a field and then mutating it without any invariant checks).
I don't know if there are any solutions combining this with static analysis. Of course, even the runtime checks are very helpful (doubly so in AI-written code).
I especially appreciate the trick of asserting the intermediate truth to help the prover along.
As someone who writes software I very much agree that verification of asserts before run time (written in the language itself) is very approachable to a programmer.
In a similar vein I agree with the folks at Jane Street that aiming to rule out specific classes of bugs (as opposed to proving a program is entirely correct) is a very practical goal.
Have you looked at "Verified Design-By-Contract"? See the paper Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm by David Crocker here - https://www.eschertech.com/products/verified_dbc.php
Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime.
At the same time their take on loops (you can't write them and have verification puts me off). Especially when modern c++ has so many prebuilt looks. It would seem to me it should just be a matter of annotating the prebuilt loops and encouraging their use.
I think their approach will fail on modern encryption code because it takes too much control (loops) from the programmer.
Which paper did you read? The "Safe Object-Oriented ..." one that i pointed to or something else? Crocker's writings explain a lot more especially w.r.t. usage with C/C++.
Animats was bemoaning that OO has declined and that you needed object/DS invariants. I was pointing to the fact DbC has it all (people should always use the runtime checking approach) and with Verified-DbC you could do it statically too. Formal Methods can be done at various levels and a developer can choose and adopt what he feels comfortable with initially before graduating to fullblown heavyweight methodologies/tools. What is needed is developing Formal Method Thinking. See the paper On Formal Methods Thinking in Computer Science Education linked to here - https://news.ycombinator.com/item?id=46298961
How does it follow that there is no point in trying for formal correctness? In many problems there is an interesting subset that is quickly solvable even when the general case is not.
SAT solvers in practice are quick on just about everything.
SAT solvers being programs that solve the original NP-compete problem.
reply