[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.