Lambda the Ultimate

Guido van Rossum is recounting the history of Python as a series of blogposts. It's off to a good start.
http://python-history.blogspot.com/

During my entire programming career (19 years) I have been interested in programming languages, how to improve and implement them. I am not formally trained in compiler theory, but have implemented a number of compilers/interpreters for a number of domain specific languages during this time. Now I am pregnant to bursting with a new language, which I need to discuss/present to someone, and I hope that LtU is the correct forum to do so (I can see from the posts that a lot of highly gifted people are lurking, so I hope to get thoughtful feedback).

The language is currently under development, so it is not fully specified. My hope was to submit papers to OOPSLA in march with a working prototype, alas it does not look like I can make it happen. Still I cannot go on for another year without releasing something about Dawn. Enough said about me and my motivations...

I will post a couple of times under this topic, with the various aspects of the language, to discuss it with the distinguished members of LtU.

Benjamin Werner explore a type theory that, among other things, might be a first step towards making a proof assistant that's also a more traditional programming environment in On the Strength of Proof-Irrelevant Type Theories, Logical Methods In Computing 2008.

Abstract. We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlying a theorem prover. We also show a close relation with the subset types of the theory of PVS. We show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is, almost classical logic. Finally we describe a simple set-theoretic semantics.

A suggested application lies a few paragraphs in.

In order to identify more terms it thus is tempting to [integrate] program extraction into the formalism so that the conversion rule does not require the computationally irrelevant parts of terms to be convertible.

In what follows, we present and argue in favor of a type-theory along this line. More precisely, we claim that such a feature is useful in at least two respects. For one, it gives a more comfortable type theory, especially in the way it handles equality. Furthermore it is a good starting point to build a platform for programming with dependent types, that is to use the theorem prover also as a programming environment. ...