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.
> [...] 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.
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.)