Static typing in programming languages are propositions[1] that the type checker proves (because it is a prover of sorts). It's very simple; it has to be simple

Static typing in programming languages are propositions[1] that the type checker proves (because it is a prover of sorts). It's very simple; it has to be simple to ensure that it's reasonably fast and above all, terminates with a clear yes/no. It's a bit off for this article not to mention that whatever cleverness underlies these examples, things will fail. That is it may not terminate in general, and if it does it might well do so without proving anything useful. I really, really like the idea of formal methods and I would really, really love to use them but they don't come for free unfortunately. [1] in an informal sense, perhaps calling them proposals might be better