That&#x27;s correct in theory, but in practice I&#x27;d be very surprised to see a useful program that couldn&#x27;t be verified by ZFC. The only natural way to get such programs is by encoding metamathematics, like trying to verify the consistency of ZFC itself.