11 Feb 2006 15:27:57 -0500

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

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.