6 ms·

Minor nit: > The job of a compiler error message is to prove to the user that their code is invalid The job of the compiler error message is to convey why the

Minor nit: > The job of a compiler error message is to prove to the user that their code is invalid The job of the compiler error message is to convey why the compiler couldn’t demonstrate the code is correct. The code may be valid but the compiler just can’t prove it (analyses are sound but not complete unless the language is strongly normalizing)

PaulHoule 1y ago
Practically the difficulty of generating error messages is one reason why "we can't have nice things". I ran into this problem while trying to write an adventure game (like Zork) in Drools. Drools sucks in a lot of stuff from a Java compiler and mashes it into a production rules framework and the result is I was getting error messages that made no sense at all and thus gave up on the project. One approach to compiler development is one of successive transformations and it is possible to cut compilers into very thin slices like the original FORTRAN for the IBM 1401. Similarly you can go beyond the methods taught in Graham's On Lisp to do rather complex metaprogramming in Lisp or some other language, trouble is that an error manifests at stage N+5 but the information required to explain what went wrong was elided at stage N so it is quite difficult to figure out what's going wrong.
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 ago
  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 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 ago
    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 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 ago
        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 1y ago
        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 1y ago
        Again, I didn’t intend the mathematical definition of “prove.”
layer8 1y ago
One way of formally defining a programming languages is as the set of strings accepted as programs by the compiler, or by the formally defined algorithm that is implemented by the compiler. By such a definition, a given string is not a valid program of the respective programming language if the algorithm rejects it. And it is useful for the error message to show how the input program fails the requirements of the algorithm. The input program may be sound in type-system terms, but still not valid for the respective programming language.

PaulHoule 1y ago

Practically the difficulty of generating error messages is one reason why "we can't have nice things". I ran into this problem while trying to write an adventure game (like Zork) in Drools. Drools sucks in a lot of stuff from a Java compiler and mashes it into a production rules framework and the result is I was getting error messages that made no sense at all and thus gave up on the project. One approach to compiler development is one of successive transformations and it is possible to cut compilers into very thin slices like the original FORTRAN for the IBM 1401. Similarly you can go beyond the methods taught in Graham's On Lisp to do rather complex metaprogramming in Lisp or some other language, trouble is that an error manifests at stage N+5 but the information required to explain what went wrong was elided at stage N so it is quite difficult to figure out what's going wrong.

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 ago
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 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 ago
  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 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 ago
      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 1y ago
        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 1y ago
        Again, I didn’t intend the mathematical definition of “prove.”

layer8 1y ago

One way of formally defining a programming languages is as the set of strings accepted as programs by the compiler, or by the formally defined algorithm that is implemented by the compiler. By such a definition, a given string is not a valid program of the respective programming language if the algorithm rejects it. And it is useful for the error message to show how the input program fails the requirements of the algorithm. The input program may be sound in type-system terms, but still not valid for the respective programming language.