On the Programs / Proofs analogy -------------------------------- A program is not a proof. The proof that a program has a type is a proof. If the proof is trivially derivable from the program, we can slip a bit and say that the program is the proof. So, we shouldn't say, This program proves that this type is inhabited. Rather, we should say, This program, along with the proof that it has this type, proves that this type is inhabited. If types and programs are non-trivial, then the proofs that programs have types will be more difficult. In fact, they may not be easily derivable from the programs alone. More expressive types --------------------- Types are specifications. I would like to see much more expressive type systems. The user should be able to postulate interesting properties of programs and prove that they hold. Why should we be limited to properties in some fixed type language?