> Any property that you can actually be confident about, you can encode into the type system. The big theoretical drawback is that you get an unbounded increas

> Any property that you can actually be confident about, you can encode into the type system. The big theoretical drawback is that you get an unbounded increase in program length. The reason is that programs in a typed language are proofs, and proof length cannot be bounded above by any computable function of proposition length. The big practical drawback is that we just don't know how to explain proofs to a computer very well.