Right. Absolute guarantees can only apply to an algorithm, i.e. the abstract program, under certain assumptions about hardware and OS behavior. The correctness

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.