Tue Sep 15 21:05:47 CEST 2009
Proof Assistants / Constructive Analysis
Proof assistants have a small ``trusted core'' that's manually
verified, which is then used to bootstrap other theories. Correctness
can be proven _mostly_ in the system itself (but of course not fully
from Goedel's incompleteness).
An interesting remark about types vs. set theory: in set theory the
question: is the set \pi an element of the set \sin? (DeBruyn)
The answer depends on the encoding. You need a layer of type theory
over the set theory.
Modern proof assistants are based on type theory directly: serves both
as a foundation of mathematics and as a programming language.
Exact reals scream for constructive logic because there is no
zero-test. You want to avoid taking the exact decision P or not-P
while programming. However for naturals, rationals or other decidable
structures you do have this decision.
Programming in type theory used for real programs:
Leroy built a machine-verified compiler for Cminor (subset of C) to
machine language. The idea is to extend this to Coq (built on Ocaml
(built on C)).