The obvious part is that by the time your code stabilizes (and you have good techniques and process) then most of the faults in the code have been eliminated. A

The obvious part is that by the time your code stabilizes (and you have good techniques and process) then most of the faults in the code have been eliminated. At this point you should have an informal or formal proof of correctness with little need to take the time to get the machine to do the proof for you. > There's a lot of 'stabilized' code especially within libraries, that could be endowed with formal guarantees. Just to take this a little further consider the many open-source libraries out there written in dynamic languages and in use by thousands of production-facing business code. Perhaps there is justification in cases to apply formal techniques, but these libraries are clearly content to use other tools (informal tools, testing, release process, social processes, etc). > "lightweight" static techniques would still be useful if only as a means of avoiding egregious mistakes I'm 100% in agreement with you here. My argument is that static techniques should be looked at as nominal tools and not be put on a pedestal nor placed on the main path of continuous delivery and development as the static type enthusiasts have it.