4 ms·
But the whole point of type systems is that you can theoretically verify your code at a high level (though very few computer languages are able to approximate a
by lobster_johnson 10y ago
But the whole point of type systems is that you can theoretically verify your code at a high level (though very few computer languages are able to approximate anything like a mathematical proof).
I wrote about this in another comment, in the context of writing tests.
- kazinator 10y agoIn theory, practice is the same as theory. In practice, it isn't. I've seen only toy examples of some non-trivial program properties being encoded in type systems. It nowhere constituted proof of an entire program. Nobody actually does that. A lot can remain wrong in code which passes type checks. There is no "if it compiles, ship it". Not to mention that compilers can have bugs, and that hidden performance and resource problems can lie latent in high level languages.
- njs12345 10y agoHow about the property 'this variable is never null'? You might call this trivial but it seems to be useful given that real-world programmers get it wrong frequently: http://stackoverflow.com/search?tab=newest&q=NullPointerException http://stackoverflow.com/search?tab=newest&q=NullPointerExce... Or the property 'this variable is never used after a free' in a language with manual memory management (Rust encodes this) or 'this program is free from data races' (also Rust)? No one is arguing that strong static type systems make it impossible to write programs with bugs, but eliminating whole classes of bugs at compile time certainly makes it easier.