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 f

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.