There doesn't seem to be anything like a conversion rule. I suspect that a 
lot of the math examples developed in the system don't actually type check. 
If they do, it would seem to be luck. Or maybe not; does anyone know some 
key intuition behind this system that I'm missing?

On Friday, May 4, 2018 at 5:01:53 PM UTC-4, Martín Hötzel Escardó wrote:
>
> 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"
>
> This was in the late 1960's (or correct me). Here is a link to both 
> manuscripts: http://www.cs.bham.ac.uk/~mhe/Bishop/
>
> Greetings from Bonn.
> Martin
>