> Sure, and our structural engineering tools and processes no doubt similarly rule out many highly artistic and potentially safe architectural designs.

Once in a while, civil engineering has a revolution exactly because somebody proves that a class of new designs is safe. The argument is compelling on every field.

There is already finite element analysis. It basically works on arbitrarily complex structures their internal connections, loads, etc. (It enabled the current boom in super skinny high rises and various fancy structures.)

We don't really have that for programming, but it's not like we shouldn't try. (Eg we have TLA+ for processes, we can use Coq and others for proving some parts of programs.)

> We don't really have that for programming, but it's not like we shouldn't try.

We do in the form of abstract interpretation and various other global static analyses. Unfortunately, these analyses are non-compositional, where small code changes can lead to dramatic and unpredictable long-range effects in the properties of your code. Finite-element analysis has similar non-compositional properties.

A type system is a compositional form of static analysis, and composition obviously has considerable reuse and cost reduction benefits, which is probably why most programming doesn't use static analysis tools beyond type systems.

Finite-element analysis - as far as I know - has the advantage of being able to estimate its own errors with some practically useful local upper bound. Because physics at that level is very much local. (Though it can't really help with higher level problems, like cyclic dynamical load and resonance problems, but there are other tools for that.)

> [...] most programming doesn't use static analysis tools beyond type systems.

Yes, unfortunately. :( It'd be great to have access to much better/stricter tools to be able to check just some interesting/important parts of programs (eg. pure business logic modules/functions) without resorting to reimplementing them in static-analysis systems.

LiquidHaskell!

Indeed, a type system is a great tool for producing correct code, and I cannot advocate doing away with type safety. However, my counter-argument would be that important failures often occur due to unforeseen interactions in complex systems, perhaps more so than due to actual defects. If a type system precludes simple solutions ("obviously no bugs"), then that may cause problems in itself. My feeling is that type systems should be separate from the language, and should statically validate in a progressive manner (eg Typescript on Javascript). As the type system is evolved to become more expressive, the amount of unsafe code can be reduced - but never quite eliminated (if my conjecture is correct).