[pron]

Right. Absolute guarantees can only apply to an algorithm, i.e. the abstract program, under certain assumptions about hardware and OS behavior. The correctness of software, a program running in the real world, is always probabilistic. There was an interesting case of a bug in the Java and Python sorting routines (TimSort) whose probability of manifestation in practice was about the same as a failure due to some hardware malfunction (bit-flip etc.). So you could think about it as if the algorithm was completely incorrect, but the program was about as correct as when running a totally correct algorithm.

[dnautics]

I guess you could amend it to 'the type system prevents 100% of reasonably preventable errors of the class'!!