This week I learned two interesting things that seem to be kept as a guarded secret:
(1) Errett Bishop reinvented type theory.
(2) He also explained how to compile it to Algol.
I am adding a link to these two manuscripts. A nice quote from the second paper (Algol.pdf) is this, in my opinion, because it foresees things such as Agda, Coq, NuPrl, ...
"The possibility of such a compilation demonstrates the existence of a new type of programming language, one that contains theorems, proofs, quantifications, and implications, in addition to the more conventional facilities for specifying algorithms"
Greetings from Bonn.
Martin