What proofs are good for is decoupling implementation and semantic definition of software (and application specific circuits).
Like, proving that in the absence of hardware faults, some optimizer for JavaScript can never result in arbitrary memory accesses.
Or that some database doesn't violate data semantics under ANY condition.
Or that as long as not too many sensors fail, a plane autopilot will not go and do anything that would lead the plane to exceed safe speeds and forces/accelerations. (Won't just go crash the plane or drop it from the sky in one or more pieces just because some few sensors froze or caught lightning or something.)
Like, proving that in the absence of hardware faults, some optimizer for JavaScript can never result in arbitrary memory accesses.
Or that some database doesn't violate data semantics under ANY condition.
Or that as long as not too many sensors fail, a plane autopilot will not go and do anything that would lead the plane to exceed safe speeds and forces/accelerations. (Won't just go crash the plane or drop it from the sky in one or more pieces just because some few sensors froze or caught lightning or something.)