&gt; If we&#x27;re balancing a bank&#x27;s accounts, I think we&#x27;re safe.<p>You seem to be contradicting your original claim, that it is impossible to prove any non-trivial program correct. Is this because you believe the program to balance a bank&#x27;s accounts is trivial? Do you also believe that a C compiler is trivial?<p>I guess we never defined what you meant by &quot;non-trivial.&quot; If your position is that the vast majority of software in the world today is &quot;trivial,&quot; sure, I&#x27;d agree with you. But that&#x27;s not really a meaning of &quot;trivial&quot; that anyone expected.