> That “static types” are, at their core a tool for writing and maintaining computer-checked proofs about code > That “dynamic types” are, at their core, there

> That “static types” are, at their core a tool for writing and maintaining computer-checked proofs about code > That “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs. They are not rival. Imagine a gradual typing design, it has a statically typed system, but it won't stop you from running it. The type errors would only be suggested in IDEs and stop building on CI environment but you can run it anyway. Then you can have both checked proofs and debugging advantages. (Dialyzer for Erlang is an example but there could be more strict typing) Another similar topic is 'compiled' and 'interpreted', instead of static and dynamic types. 'Compiled' is runtime favored because the code was compiled is ready to be executed a lot of times, while 'interpreted' was executed once on demand because you may change your code at any time, so there's no point compile it for one person. Plus source code is much easier to debug than byte code. It would be interesting to see languages could have solid static/dynamic/compiled/interpreted at the same time. Elixir/TypeScript/F#, etc. are good examples but this idea can definitely go further.