3 ms·
If you are willing to adopt a strong enough type system pretty much any interesting property about a program you want to prove is provable. Its just a matter of
by jroesch 10y ago
If you are willing to adopt a strong enough type system pretty much any interesting property about a program you want to prove is provable. Its just a matter of ergonomics, more complex type systems provide power, but require investment in understanding, both conceptually, and in modeling your problem.
You can also adopt automated verification techniques that can prove strong properties about a system automatically.
- Silhouette 10y agoAll true, up to a point at least. Strong, static type systems aren't universal wins with no drawbacks. 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.