Re:The Deep Link Equating Math Proofs and Computer Programs
by deterministic on Friday October 13, 2023 @10:29PM
(#37877617)
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.
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.