What should a proof of correctness for a typechecker actually be proving? I've been programming for several years, but am very unfamiliar with theoretical CS. I've recently been trying to study programming languages, and as part of that, type checking and inference.

My question is, if I try to write a type inference and checking program for a programming language, and I wish to prove that my typechecker works, what exactly is the proof I'm looking for?

In plain language, I want my type checker to be able to identify any errors in a piece of code that might occur at runtime. If I were to use something like Coq to try proving that my implementation is correct, what exactly will this "proof of correctness" be trying to show?
That's a good question! It asks what we expect from types in a typed language.

First note that we can type any programing language with the unitype: just pick a letter, say U, and say that every program has type U. This isn't terribly useful, but it makes a point.

There are many ways to understand types, but from a programmer's point of view the following I think is useful. Think of a type as a specification or a guarantee. To say that $e$ has type $A$ is to say that "we guarantee/expect/demand that $e$ satisfy the property encoded by $A$". Often $A$ is something simple like int, in which case the property is simply "it's an integer".

There is no end to how expressive your types can be. In principle they could be any kind of logical statements, they could use category theory and whatnot, etc. For example, dependent types will let you express things like "this function maps lists to list such that the output is a sorted input". You can go further, at the moment I am listening to a talk on "concurrent separation logics" which allows you to speak about how concurrent programs work with shared state. Fancy stuff.

The art of types in programming language design is one of balancing expressivity and simplicity:


more expressive types allow us to explain in more detail (to ourselves and to the compiler) what is supposed to be going on
simpler types are easier to understand and can be automated more easily in the compiler. (People come up with types which essentially require a proof assistant and user's input to do type checking.)


Simplicity is not to be underestimated, as not every programmer has a PhD in theory of programming languages.

So let us come back to your question: how do you know that your type system is good? Well, prove theorems that show your types to be balanced. There will be two kinds of theorems:


Theorems which say that your types are useful. Knowing that a program has a type should imply some guarantees, for instance that the program won't get stuck (that would be a Safety theorem). Another family of theorems would connect the types to semantic models so that we can start using real math to prove things about our programs (those would be Adequacy theorems, and many others). The unitype above is bad because it has not such useful theorems.
Theorems which say that your types are simple. A basic one would be that it is decidable whether a given expression has a given type. Another simplicity feature is to give an algorithm for inferring a type. Other theorems about simplicity would be: that an expression has at most one type, or that an expression has a principal type (i.e., the "best" one among all types that it has).


It is difficult to be more specific because types are a very general mechanism. But I hope you see what you should shoot for. Like most aspects of programming language design, there is no absolute measure of success. Instead, there is a space of design posibilities, and the important thing is to understand where in the space you are, or want to be.