Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: Formal Proof Language Example - Human-Readable?
Replies: 39   Last Post: Jun 27, 2009 11:09 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Spiros Bousbouras

Posts: 51
Registered: 9/18/08
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 6:24 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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 Mizar-like 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
C-like 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


Date Subject Author
6/21/09
Read Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/26/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Joshua Cranmer
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Marshall
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Spiros Bousbouras
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Tim Smith
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Charlie-Boo
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
William Elliot
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/23/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
David Bernier
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.