Return to the
comp.compilers page.
Search the
comp.compilers archives again.
| 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] |
| 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
Return to the
comp.compilers page.
Search the
comp.compilers archives again.