Neither is static typing. It's a layer of protection, much like tests.
Proofs are exactly what the results of strong static type systems give you. They can't prove everything, but they do prove certain things in all possible cases.
Neither is static typing. It's a layer of protection, much like tests.
Proofs are exactly what the results of strong static type systems give you. They can't prove everything, but they do prove certain things in all possible cases.
You can also adopt automated verification techniques that can prove strong properties about a system automatically.
However, I think it's fair to say that even the "strongish, staticish" type systems in a lot of mainstream languages can still prove very useful properties that are often sources of bugs in the more dynamic languages. A good example would be not accidentally allowing null values to be passed around, as mentioned elsewhere in this discussion. And of course some of less well known but still not uncommon languages, such as the popular functional programming choices or newer offerings like Rust, can do quite a lot more without their type systems becoming an unreasonable burden.
Much like tests then?
Static type guarantees are actual proofs (barring a compiler bug), and they narrow down the domain that your tests have to probe.