What's the relationship between "semantic type soundness" and "functional correctness"?

Question

In the Milner Award lecture "The Type Soundness Theorem That You Really Want to Prove (and now you can)" and related Sigplan blog post (with collaborators), Derek Dreyer argues that semantic soundness is an important thing worth proving.

In the questions section, Adam Chlipala asked how to trade off complexity between proving soundness of semantic types and functional correctness, and Dreyer unfortunately said "let's take this offline," so I don't know what the answer is.

Is the answer "semantic type soundness is something to prove about a programming language, but functional correctness something one proves of a program"?

I'm still a bit confused, though, because then someone asked a follow-up question about how semantic type soundness could fail to hold. Dreyer's answer was that if someone were to add a covfefe rule that flipped an arbitrary int to 0, it could trigger someone's assertion that under certain conditions a given int is never 0. So this makes it sound like soundness proofs for semantic types do involve the details of particular programs.

In addition to an answer to Adam Chlipala's question, it would be helpful to have some simple reference for what "semantic type soundness" means - the blog post doesn't really define it, and the closest paper I could find was the RustBelt paper which only discusses "semantic type soundness" in the context of a Rust MIR-like language and Iris, but I couldn't find a more general definition.

Answer 1

I'm not an expert, but can give at least a partial answer since I've been reading about this lately. The more recent preprint A Logical Approach to Type Soundness gives a good overview of what this is all about, outside the specific context of Rust.

The key distinction is between two relations: syntactic type checking ($\Gamma \vdash e : \tau$), which is the syntax-directed type checking we're usually familiar with, and semantic type checking ($\Gamma \vDash e : \tau$) . Roughly speaking, an expression $e$ semantically type checks as type $\tau$ if at run-time it eventually evaluates to a value with type $\tau$. Of course in general that reduces to the halting problem and is just as hard as any other kind of functional correctness proof.

I could be misinterpreting, but I think what Adam is asking is "The proof system you've shown here isn't powerful enough to prove all functional correctness properties, so how do you design a proof system that's 'good enough' to prove most of the stuff you need for semantic type checking, but not overly powerful/general?". I suspect the answer is along the lines of "it's a tradeoff, and there are many valid points you could select on the spectrum from very simple to very complex proof system", and so getting to the details of that question requires taking it offline.

Re: proving about a program or a language: Yes, semantic type soundess is something you would prove about a language as a whole. Semantic type soundness means that whenever a program semantically type checks, then it is always "safe" to run that program (for some definition of safe). However, whether an individual program semantically type checks is something you prove about a single program, and can sometimes require proving functional correctness of that program.

The first few sections of the "Logical Approach" paper above give a nice description of this, so I recommend checking it out if you'd like more details.