Actually, joel_ms is correct; you can encode these "dynamic" properties of values in a static type system, in the same way that you can prove properties about a

Actually, joel_ms is correct; you can encode these "dynamic" properties of values in a static type system, in the same way that you can prove properties about a program on paper without actually running it. The connection between programs and proofs [1] is rather mind-blowing to learn about, and unfortunately no popular programming language supports this style of "certified" programming. But there are some interesting languages which do, such as Idris and Coq. [1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...