I agree that validation is important (e.g. avoid optimising things which shouldn't exist https://youtu.be/t705r8ICkRw?t=1022 https://youtu.be/t705r8ICkRw?t=1022

I agree that validation is important (e.g. avoid optimising things which shouldn't exist https://youtu.be/t705r8ICkRw?t=1022 https://youtu.be/t705r8ICkRw?t=1022 ). It's all about bang-for-buck: a formal proof can give me lots of confidence about some aspect of a system, but might take a long time and have a maintenance burden; if that time and maintenance could give me more confidence when used to write masses of tests instead, then it's probably better to go with the tests. My go-to approach is property-based testing, since that can exercise edge-cases more effectively than hand-picked examples, whilst taking about the same amount of effort to write. A couple of things in favour of "proper" formal methods (in niche circumstances): - Sometimes the effort calculation tips in favour of a formal methods; e.g. reliably testing concurrent, distributed systems is notoriously hard, and might require even more effort than doing some proofs instead. - Proof objects themselves, and the act of writing them, can be useful for understanding a domain or system, and why certain things are/aren't true. This doesn't apply so much for "yes/no" solvers, like SAT/SMT/resolution/etc. but is often the case for "interactive" systems like Coq/Agda.