> Well, maybe. Additional costs with these approaches are often ignored. I wouldn't want to give up proof systems as a tool, but too many treat them as a zero cost panacea. A proof system or type checker is not an excuse to not give a fk about your craft, but I've seen it that way more frequently than I'd like to admit.

The acceptable defect rate to the business is presumably fixed, so if a proof system or type system reduces you defect rate below that then that should be an "excuse" to write fewer tests and move faster, as icky as it feels to do that. I find the maintenance burden of tests is often underestimated; types in particular may not be free, but they get you more bang for your buck than any alternative, in my experience.

> Personally and honestly, outside of already well understood or defined systems, I'd say that people should invest their time in understanding their business domain, before they dig deep into proofs and related techniques.

Isn't it the same thing though? Encoding your business domain into the system you're using is the hardest part of using any formal system, but it's also an excellent way of forcing you to really understand the domain.