Re: Compiler Correctness

haberg@math.su.se (Hans Aberg)
11 Feb 2006 15:27:57 -0500

          From comp.compilers

Related articles
[3 earlier articles]
Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-07)
Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-11)
Re: Compiler Correctness danwang74@gmail.com (Daniel C. Wang) (2006-02-11)
Re: Compiler Correctness torbenm@app-1.diku.dk (2006-02-11)
Re: Compiler Correctness henry@spsystems.net (2006-02-11)
Re: Compiler Correctness Sid.Touati@inria.fr (Sid Touati) (2006-02-11)
Re: Compiler Correctness haberg@math.su.se (2006-02-11)
Re: Compiler Correctness haberg@math.su.se (2006-02-11)
Re: Compiler Correctness henry@spsystems.net (2006-02-11)
Re: Compiler Correctness Xavier.Leroy@inria.fr (Xavier Leroy) (2006-02-12)
Re: Compiler Correctness DrDiettrich@compuserve.de (Hans-Peter Diettrich) (2006-02-14)
Re: Compiler Correctness marcov@stack.nl (Marco van de Voort) (2006-02-14)
Re: Compiler Correctness DrDiettrich@compuserve.de (Hans-Peter Diettrich) (2006-02-14)
[5 later articles]
| List of all articles for this month |

From: haberg@math.su.se (Hans Aberg)
Newsgroups: comp.compilers
Date: 11 Feb 2006 15:27:57 -0500
Organization: Mathematics
References: 06-02-053 06-02-061 06-02-068
Keywords: theory
Posted-Date: 11 Feb 2006 15:27:57 EST

"Daniel C. Wang" <danwang74@gmail.com> wrote:


> A minimal proof verifier is 1-2 thousand lines of C code. This proof
> verifier uses no library calls. It's designed so you can compile it to
> assembly and can eyeball the output of the compiler. The basic logic
> has around 10 axioms from which all of modern mathematics can be
> derived.


I did not know that mathematicians had agreed on a set of axioms from
which all known mathematics can be derived. :-) Would you mind
specifying these axioms?


Further, a theorem prover as MetaMath <http://us.metamath.org/> does
not use the Hilbert axioms straight off as written, but a
modification, and does not specify in exact what manners there results
a mathematical difference, if one. Perhaps it is not known. One
problem in the context, is that the metamathematical axioms are often
written as infinite sets of axioms, which in a computer context must
be properly rewritten as substitution axioms. The details here, seems
to be glossed over.


--
    Hans Aberg


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.