|
|
|
|
|
|
by deterministic
1 day 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. |
|
|