So why don’t we have type systems where “if it compiles, it works”?
Because there is no information in the program about what constitutes “working”. We do have type systems where “if it compiles, it never crashes”, but “not crashing” is a very weak form of “works”.
Some languages let the programmer write assertions about what the program should do, even compiler-checkable assertions, but that just pushes the problem up one level: there is no information available to the compiler about whether these are the right assertions.
Nothing stops me from writing A+B when what I wanted was A*B.
Nothing stops me from writing A+B when what I wanted was A*B.
That’s perfectly true, but if express at a high level my requirements, it would be theoretically possible for a compiler to tell me that using A*B will not achieve those requirements, halting problem notwithstanding.
Isn’t that just pushing the problem up a level with assertions? It’s only an advance if the assertions are somehow more perspicuous to the developer writing them. In fact, finding such assertions, ways of thinking about the task, is a large part of the development process.
A program has necessary complexity proportional to how complex it is to even express the task it needs to carry out, and implementational complexity, related to the difficulty of actually implementing that in practice. The total complexity is the sum of the two.
For example Conways game of life is extremely simple to state, and it should be relatively simple to express the relationship between the current state and the next to a compiler. There is a wealth of literature on how to actually implement it efficiently however, which is far from simple.
By having the compiler prove that your actual code matches the specification you provide, you can safely make the implementation as complex as you like whilst knowing it still matches the spec. For problems with low implementational complexity, that’s not a problem that needs solving, but for those with high implementational complexity it is.
Think of it like unit tests—unit tests can often take far longer to write than the program itself, but once you have them you can much more confidently change the program knowing you want adversely affect the behavior you’re interested in. Similarly a good spec of a program can take a long time to write, but in our theoretical language, you will now be able to safely change the program knowing the compiler will catch you with certainty if you make any mistakes.
Because there is no information in the program about what constitutes “working”. We do have type systems where “if it compiles, it never crashes”, but “not crashing” is a very weak form of “works”.
Some languages let the programmer write assertions about what the program should do, even compiler-checkable assertions, but that just pushes the problem up one level: there is no information available to the compiler about whether these are the right assertions.
Nothing stops me from writing A+B when what I wanted was A*B.
That’s perfectly true, but if express at a high level my requirements, it would be theoretically possible for a compiler to tell me that using
A*Bwill not achieve those requirements, halting problem notwithstanding.Isn’t that just pushing the problem up a level with assertions? It’s only an advance if the assertions are somehow more perspicuous to the developer writing them. In fact, finding such assertions, ways of thinking about the task, is a large part of the development process.
A program has necessary complexity proportional to how complex it is to even express the task it needs to carry out, and implementational complexity, related to the difficulty of actually implementing that in practice. The total complexity is the sum of the two.
For example Conways game of life is extremely simple to state, and it should be relatively simple to express the relationship between the current state and the next to a compiler. There is a wealth of literature on how to actually implement it efficiently however, which is far from simple.
By having the compiler prove that your actual code matches the specification you provide, you can safely make the implementation as complex as you like whilst knowing it still matches the spec. For problems with low implementational complexity, that’s not a problem that needs solving, but for those with high implementational complexity it is.
Think of it like unit tests—unit tests can often take far longer to write than the program itself, but once you have them you can much more confidently change the program knowing you want adversely affect the behavior you’re interested in. Similarly a good spec of a program can take a long time to write, but in our theoretical language, you will now be able to safely change the program knowing the compiler will catch you with certainty if you make any mistakes.