>What all of these “obviously correct” methodologies ask you do is to sacrifice varying degrees of expressiveness at their altar.
In the case of static types, this is simply untrue. Embedding dynamic types into static type systems is a triviality. With compiled code, there is generally a substantial speed up at runtime assocaited with a good static type scheme.
I think this is missing the point. On a practical level, most of these "obviously correct" methodologies have escape hatches: i.e. FFIs for memory safety. On a theoretical level, by embedding dynamic types in a statically typed language, you have a stratification where code written in the host typing is "clear of typing bugs", but code written in the embedded typing is less sound. You need to distinguish between these two layers.
The point made in the OP is that expressiveness is sacrificed by having these safety features. This is simply not the case with static typing, because of the ease with which dynamic typing is embedded in a static type system.
"code written in the embedded typing is less sound" - Well the point maybe is that static typing did not bring quite the safety some thought it did: it only promised that these functions must return, if they do return, a value of a given type. The ability to model dynamic typing inside static typing shows just how weak this guarantee can be. More generally, it show there is no expressiveness sacrifice.
I think the crux of the issue here is "triviality."
I claim that it is nontrivial to embed dynamic types in a statically typed language. Usually this is due to the need to add lots of explicit coercions in order to interface with all of the code is actually statically typed. I can embed a dynamically typed programming language in my statically typed language, with its own libraries, but that's hardly "trivial".
Difficulty matters. Otherwise I can claim that I can bypass memory safety by writing a simulator for x86 in a memory safe language, and, well, the code that runs might violate memory safety (in some alternate sense), and thus, there is no expressiveness sacrifice!
"lots of explicit coercions" - even without recourse to generics, the overhead tends to be small. Really, try it. There's no need to write intepreters, let alone architecture simulators.
I tend to think the attraction of dynamic typing is the ability to run incomplete or ill-typed programs. If we have type inference, there is no real advantage in terms of conciseness.
What do you mean? You can map each dynamically typed function/procedure onto a statically typed function/procedure that is used in the same way. I do not see how a translation could be cleaner and more structure preserving.
In the case of static types, this is simply untrue. Embedding dynamic types into static type systems is a triviality. With compiled code, there is generally a substantial speed up at runtime assocaited with a good static type scheme.
See, e.g., http://suereth.blogspot.com/2010/07/monkey-patching-duck-typ...