
Re: Formal Proof Language Example  HumanReadable?
Posted:
Jun 21, 2009 6:24 PM


On 21 June, 18:03, Andrew Tomazos <and...@tomazos.com> wrote: > Please consider the following formal proof language example: > > package MyTheoryProof; > > using edu.mit.number_theory.*; > > theorem MyTheory > { > let N be NaturalNumbers; > > forall a, b, c in N > given > { > a^2 + b^2 = c^2; > a, b are_relative_prime; > a is odd; > } > implies > thereexists m, n in N > { > m <= n; > a = n^2  m^2; > b = 2 * m * n; > c = n^2 + m^2; > } > } > proven_by > { > ... > } > > This is written in a Mizarlike language with some formatting changes > based on the C family tree and some personal touches. > > Without any description of the language, I'm curious to know whether > you can derive the meaning of the theorem statement simply by reading > the code? The goal is for it to be both machine and human readable.
I understood it without any effort. But that doesn't mean I find it satisfactory.
1) Your notation is too verbose. For example "let N be NaturalNumbers". You could do without the "be". Also "thereexists" is too long.
2) "a is odd" and "a, b are_relative_prime" are hideous. I'd much rather have odd(a) and coprime(a , b).
3) I don't like that you are using ";" for conjunction. The established term is "and" and I see no reason to change it. Since I also do programming I can live with & or && but not ;.
4) I'd rather have if/then rather than given/implies.
Beyond these remarks I'd rather have a Lisp syntax rather than a Clike syntax so that the possibility exists for powerful macros. I think macros could be quite useful in proofs.
 Prediction: Somebody at Microsoft will throw together a script that rummages through source replacing memcpy (unto, from, size); with memcpy_s (unto, size, from, size); and will then announce that the world has become safer because the evil memcpy() has been expunged. Eric Sosman at http://tinyurl.com/mfbbuy

