nqthm

mber theory from the axioms in under a minute.[1] I fixed it up recently to run on GNU Common Lisp and put it on Github, so it's runnable on modern machines. There's certainly no excuse for inflicting Newton's notation for calculus on kids. It's not even clear that classical geometry proof approaches are that useful. [1] https://github.com/John-Nagle/nqthm

, I brought the original Boyer-Moore theorem prover back to life and put it on Github.[2] Some of our lessons learned were: 1. Integrate the verification statements into the programming language. Don't try to do it with comments. You want the language's regular syntax, type and variable checking to apply to the verification statements. We added the keywords ASSERT, ENTRY, EXIT, MEASURE, STATE, EFFECT, INVARIANT, DEPTH, and PROOF, EXTRA, and RULE. 2. Make verification program-like, not math-like. For example, if we wanted to verify the structure of a tree, we would add fields for a back-pointer and a tree depth to the data structure each node. We'd put in all the code to maintain them, and verify that the forward pointers and back pointers were consistent and that child objects always had a greater depth than their parents. This would all be done by writing ordinary-looking code with ASSERT statements. But the new data fields would have the EXTRA attribute, and the code manipulating those fields would have PROOF in front of it. This meant it was there only for verification purposes. No executable code could depend on that data, so it could all be stripped out for execution. 3. Use two theorem provers. One prover was an Oppen-Nelson decision procedure. This is fully automatic proving for integer +, -, multiplication by constants, inequalities, conditionals, logic operators, structures, and arrays. This subset of mathematics is decidable and there's a fast, complete decision procedure for it. That knocks off all the easy stuff automatically. Easy stuff usually includes subscript checks and overflow checks. The second prover was the Boyer-Moore prover, which is semi-automatic; you have to propose lemmas to help it along. This is hard. By using ASSERT statements to narrow the area of trouble, you could reach the point where you had two successive ASSERTs, one of which should imply the other, but the Oppen-Nelson prover couldn't prove it and there was no previously proved rule on file to cover it. But now the problem had been narrowed to an abstract mathematical problem - prove the second ASSERT from the first. Someone could work on that in the Boyer-Moore prover and then export the rule for use in the main system. This provided a separation of functions - you could have mathematically oriented people to struggle with the theorem prover, independent of the code. You could reuse that rule elsewhere, and change other code without having to re-prove it. Today, we'd put files of useful theorems on Github. We never let the user add "axioms". That opens a huge hole. 4. Expect to do a lot of compiler-type analysis and bookkeeping as part of the verification process. For example, the static analysis to determine that a function is pure ("pure" means x = y implies f(x) = f(y), and no side effects.) is something to do as a routine compiler operation. Potential aliasing has to be discovered. Do this using compiler techniques; don't dump it into the theorems-to-be-proved mill, where it's much harder to give the programmer good error messages. 5. Don't fall in love with the formalism. Too much work in verification has been done by people who wanted to publish math papers, not kill program bugs. This is about creating bug-free code. I think people will get this now, but when I was doing this, everybody else involved was an academic. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf [2] https://github.com/John-Nagle/nqthm/tree/master/nqthm-1992