The Lean Theorem Prover

It is an exciting time at the crossroads of Mathematics and Programming. The Lean Theorem Prover (http://leanprover.github.io/) looks very useable for what Wombat needs. To quote from an earlier post (Whither Wombat):

More substantively is the issue of the status of laws/axioms. It used to be that these were just comments. Then languages started including them in an executable form, with a bit of handwaving “quickcheck style checking programs might use this”. That’s where Wombat came in, and the way it is specified in the doc.

But I don’t think this phase will last long. It is time to do it properly and prove all claimed properties:

• Primitive types will come with axioms describing their behaviour, from the X86/JVM/whatever manual.
• The semantics of other Types will be proved from the code implementing the semantics using the assumed (if primitive) or proved (if not) semantics of the implementation.
• Other things that need to be proved include:
• proving that a supplied specialization does indeed implement the same algorithm as the original;
• proving that the procedures linking one implementation to/from a more comprehensive one (usual the main one) are inverses (where the reverse is defined).
• …

The hope, with respect to Lean, is that the Wombat compiler will be able to call the Lean API to perform these proofs. In many cases one would hope that Lean will just work out the proof itself. If not one would hope that the programmer can use the Lean interactive mode to construct a proof which can be included in the program. I suspect this is all a bit ahead of its time, but it would certainly be interesting to try to get it going in a small subset of Wombat.