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)).

[1] http://videolectures.net/aug09_spitters_oconnor_cvia/