A (perhaps) bigger problem with the single-mindedness around the progress/preservation type soundness is that it relies (fundamentally) upon “not going wrong” at runtime actually meaningfully capturing whatever static invariants your type system was supposed to enforce.
For example: let’s say you come up with a fancy new type system to enforce array bounds checks statically. Since you did this to make your language fast, you don’t check anything at runtime. But, to ensure this is safe, you prove that your type system is sound, and all is well. Except all this naive “type soundness” result will say is that you don’t get “stuck”, and you (intentionally) don’t actually check anything at runtime to ensure that you are within bounds, so you never get stuck anyway: your soundness theorem is meaningless. It would only actually tell you something if you actually checked every access for boundedness and failed (got “stuck”) on any out-of-bounds access. In that case, not getting stuck actually means that you never go out of bounds, and your type system does something.
Of course, a more sensible approach is probably to change the theorem itself, so that rather than generic “stuckness” (which then requires you to augment the runtime semantics with stuff you don’t want it to have), you actually describe what behavior you want not to occur.
A (perhaps) bigger problem with the single-mindedness around the progress/preservation type soundness is that it relies (fundamentally) upon “not going wrong” at runtime actually meaningfully capturing whatever static invariants your type system was supposed to enforce.
For example: let’s say you come up with a fancy new type system to enforce array bounds checks statically. Since you did this to make your language fast, you don’t check anything at runtime. But, to ensure this is safe, you prove that your type system is sound, and all is well. Except all this naive “type soundness” result will say is that you don’t get “stuck”, and you (intentionally) don’t actually check anything at runtime to ensure that you are within bounds, so you never get stuck anyway: your soundness theorem is meaningless. It would only actually tell you something if you actually checked every access for boundedness and failed (got “stuck”) on any out-of-bounds access. In that case, not getting stuck actually means that you never go out of bounds, and your type system does something.
Of course, a more sensible approach is probably to change the theorem itself, so that rather than generic “stuckness” (which then requires you to augment the runtime semantics with stuff you don’t want it to have), you actually describe what behavior you want not to occur.
I found the companion lecture quite good, with some nice “proof”-by-animation.