Re:The Deep Link Equating Math Proofs and Computer Programs
by Tainnor on Wednesday October 11, 2023 @03:10PM
(#37848926)
We run proofs on code all the time, it's called type-checking.
What you mean is that it's practically infeasible to verify every program behaviour we're interested in. That's probably true for large enough programs, but it doesn't mean we can prove nothing about them.
What you mean is that it's practically infeasible to verify every program behaviour we're interested in. That's probably true for large enough programs, but it doesn't mean we can prove nothing about them.