Lambda the Ultimate

Retrospective: An Axiomatic Basis for Computer Programming, by C.A.R. Hoare:

This month marks the 40th anniversary of the publication of the first article I wrote as an academic. I have been invited to give my personal view of the advances that have been made in the subject since then, and the further advances that remain to be made. Which of them did I expect, and which of them surprised me?

An interesting review of the history of computing. He has some nice perspectives on the complementarity of testing and formal methods, and how the growing cracking industry became an unexpected driving force behind industrial interest in verification.

After going through both of the Types and Programming Languages books, I am starting to feel confident in my understanding of Type Systems in terms of how they would be implemented. However, I still feel uncomfortable with the theoretical foundations; even after going through the proofs it still seems like a lot of hand-waving when defining what is a type. So to try to find a good mental model of what a type is I thought I would ask LtU: what is a type?

The reason for my uneasiness probably stems from my background programming in both static and dynamic type systems. The static definition of types seems to tend more towards what can be proven at compile time. This definition seems to put more emphasis on creating type systems which are strongly normalizing. However, in dynamic type systems, types are often manipulated as terms. Trying to find a consistent mental model for these two usages of the term (especially after the introduction of subtyping) I am currently stuck with defining them as propositions which map terms to truth values. The intuition is that a type is a proposition, nothing more. I can't seem to find much theory for such a model and that prompted this post. Is this highly inconsistent with current theory?

More formally, what would your initial reaction be to a system where:

λt:T.x  →  λt. if T(t) then x else TypeError