|
|
|
|
|
|
by deterministic
975 days ago
|
|
|
It doesn’t matter. What matters is if you can prove things you care about true for code you care about. And yes we can prove termination and zero bugs for a lot of practical useful code. Examples: seL4 is a proven correct micro kernel and CompCert is a proven correct C compiler. The trick is to use programming languages that are total i.e. not general infinite tape turing machines. |
|
|