Every beginning student of programming—that is, every student with the ill fortune of having a language with a static type system foisted upon them by a well-intentioned yet sadistic instructor—is well-acquainted with the Dreaded Type Error Message. Why do type error messages have to be so terrifying? Can’t we do a better job explaining type errors to programmers?

We propose two interrelated theses:

• We ought to move away from static error “messages” and towards interactive error explanations.
• We ought to consider the problem of generating error explanations in a more systematic, disciplined, and formal way. Explaining errors to users shouldn’t just be relegated to the status of an “engineering issue”, but ought to have all the tools of programming language theory and practice applied to it.