[tshaddox]

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]

It 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]

> 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]

A 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]

> I could rephrase it as "the goal...is to demonstrate to the user what is invalid about their code."

This is closer, yes.

[tshaddox]

To 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]

The 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]

Again, I didn’t intend the mathematical definition of “prove.”