[Someone]

Would you drive (aka 'use') a robotic car without a roll cage, safety belts, crumple zones and air bags because its software is proven correct? I would not.

I think the way to go is to augment the model for what the function does with its behavior on erroneous inputs, and change to source code so that the prover can prove that the code implements the more robust model.

[kd0amg]

Exactly what sense of "correct" are we assuming has been proven? The correctness is obviously not that the car cannot be involved in a collision.

[Someone]

Why would that be obvious? It would require way more work to prove, but I think I could define a set of rules about the world and a control mechanism for an autonomous vehicle that guaranteed there would never be a collision at dangerous speed (Getting that work at reasonable speed and with enough 9s of availability to make the thing practical will be even more work)

Problem is, the assumptions that such a model makes will be violated, either because the world is different than modeled or due to failure of a component. That is why you would want additional safety features.

That, IMO, is similar to the case where you build a component for base64 encoding, prove that it never will be called with a null pointer argument, and yet include that null pointer check and a way to signal errors in your component.

You can be sure "It will never happen" _will_ at some moment turn into "that's interesting", but you don't know where or when.

[kd0amg]

Why would that be obvious?

A straight up "no collisions" theorem would require proving limits on the behavior of other objects in and around the road and also that certain mechanical components never fail.

[Someone]

Again, just as in the base64 program. It is proven correct only in a world without cosmic rays, oxydation, failing capacitors, etc.

The 'only' difference is one of scale (orders of orders of magnitude.)

[kd0amg]

The scale difference is the difference between trivial and serious. Cosmic rays aren't nearly as much a hazard of day-to-day programming as other cars are of day-to-day driving.