I said “formally”, not “with types”. I firmly believe in using the right tool for the job, and some things are best handled with manual proofs. As helpful as types might be for computer-generated proofs (type inference), I'd rather carry out my manual proofs using good old-fashioned predicate logic. Some proof techniques still need to be backed up by type structure, though (e.g., induction over datatypes).
> Every other program in every other languages has most of its meaning expressed informally, in the mind of the programmer.
Unfortunately, I can't read minds. I can only read proofs that have been explicitly written down.
> Unless you believe that no programs work, then nearly all programs that do express most of their meaning informally.
My definition of “work” is “works in all cases”. No bugs. No unforeseen cases.