4 ms·
People do use formal methods. Type checking is a simple form of formal methods. Some languages have type systems that are advanced enough to prove code correct
by deterministic 2mo ago
People do use formal methods. Type checking is a simple form of formal methods.
Some languages have type systems that are advanced enough to prove code correct (LEAN/Agda/...)
Other examples are seL4 (a proven correct micro kernel used on millions of devices), CompCert (a proven correct C compiler used by Airbus), TLA+ used by AWS etc. There are many more examples.
So yes it is not main stream but it is being used where it counts.