Re:The Deep Link Equating Math Proofs and Computer Programs
by staunton on Wednesday October 11, 2023 @02:17PM
(#37848200)
What does it mean to say "a program is provable"? You have to prove something about it.
In principle, nothing prevents you from taking e.g. an ARM binary and formally proving that it will never crash in some environment, e.g., bare metal chip with known amounts of memory etc. This is very hard for useful programs and not worth it in pretty much any application there ever was, but it's possible and getting ever easier over time.
In principle, nothing prevents you from taking e.g. an ARM binary and formally proving that it will never crash in some environment, e.g., bare metal chip with known amounts of memory etc. This is very hard for useful programs and not worth it in pretty much any application there ever was, but it's possible and getting ever easier over time.