This part (which is tangential to the real thesis of the paper) is interesting: > Advocates of strong type checking in compiled languages have attempted for ye

This part (which is tangential to the real thesis of the paper) is interesting: > Advocates of strong type checking in compiled languages have attempted for years to build compilers capable of proving the type correctness of programs. We believe that they have failed. All languages sophisticated enough for serious programming require at least some dynamic checks for type safety at execution time. In 1986, languages such as Miranda and ML existed in reasonably serious forms, and clearly had sound type type checkers and quite powerful type systems, including parametric polymorphism. Does the paper take the stronger position of counting things like array indexing as part of "proving type safety", or was there still a conception in 1986 that "serious programming" could not be done in a type-safe manner? It is definitely true that even in 2022, the vast majority of statically typed languages still perform run-time safety checks for some operations, such as integer division and array indexing. While languages that support fully provably safe programming exists, they are clearly in the tiny minority and not widely used, and still have ergonomic problems.