3 ms·
Sure, but the goal when designing a compiler and its error messages is to prove to the user that their code in invalid. Most practical type systems are going to
by tshaddox 1y ago
Sure, but the goal when designing a compiler and its error messages is to prove to the user that their code in invalid. Most practical type systems are going to be either unsound or incomplete (or both), but the goal should be to make encountering those limitations rare in practice.
- AnimalMuppet 1y agoIt seems to me that, if the limitations are encountered too often in practice, then people stop using that language to write that kind of code, because it's too frustrating to use that way.
- LoganDark 1y ago> Sure, but the goal when designing a compiler and its error messages is to prove to the user that their code in invalid. The goal when designing a compiler and its error messages should be to give the user the information they need to correct their code.
- tshaddox 1y agoA distinction without a difference. Perhaps "prove" is sounding too mathematical. I could rephrase it as "the goal...is to demonstrate to the user what is invalid about their code."
- LoganDark 1y ago> I could rephrase it as "the goal...is to demonstrate to the user what is invalid about their code." This is closer, yes.
- tshaddox 1y agoTo prove is to demonstrate, and the way to do it is to display information about what is invalid about the code. So all these ways of phrasing it are synonymous.
- antonvs 1y agoThe meaning of "proof" in a computer science context is much stronger than that. A proof does involve demonstration, but it's demonstration via a deductive logical argument that shows that the conclusion is logically guaranteed to follow from the premises. Compiler error messages would be a lot more verbose if they did that rigorously.
- tshaddox 1y agoAgain, I didn’t intend the mathematical definition of “prove.”