back

by layer8·15d ago·view on hn ↗
Trust in formal reasoning is necessarily always conditional. You have to start somewhere. The good thing about verified formal proofs is that the only way they can be in error is if the verifier is faulty. This drastically limits the possible reasons for error.

(In practice, there’s also the possible error that the proved formal statement means something different than what you thought it meant.)