Re: Compiler Correctness
- From: haberg@xxxxxxxxxx (Hans Aberg)
- Date: 11 Feb 2006 15:27:57 -0500
"Daniel C. Wang" <danwang74@xxxxxxxxx> 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
.
- References:
- Compiler Correctness
- From: pramod
- Re: Compiler Correctness
- From: Neelakantan Krishnaswami
- Re: Compiler Correctness
- From: Daniel C. Wang
- Compiler Correctness
- Prev by Date: BCS-FACS Seminar on Programming Language Semantics, 3 March 2006, London, UK
- Next by Date: Re: Compiler Correctness
- Previous by thread: Re: Compiler Correctness
- Next by thread: Re: Compiler Correctness
- Index(es):
Relevant Pages
|
|
