[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.”