by rramadass | 2025-08-01 08:22:10+00:00
There is a nuanced but distinct difference in my use of the word Proof as used in Program as a Proof and Proof in a Mathematical Algebraic System which you have missed. They are isomorphic but not exact (hence my using the phrase it depends and scare-quotes around "proving").

The reason is because Mathematics deals with ideal and abstract objects whereas objects in the real world (eg. a computer program) can only map to aspects of the ideal world and not in its entirety.

To elaborate; a mathematical algebraic system is a set of objects and a set of operations defined on them. Axioms using those objects/operations are then defined and then inference/reasoning rules using these are defined to prove theorems in the system. There are various techniques for constructing proofs (eg. direct, induction, contradiction etc.) but all of them must map back to the domain of definition of the objects in the algebra to be considered valid and sound in the real world.

As an example, the axiom of associativity w.r.t. addition holds absolutely in mathematics when applied to {N, +} where N is the infinite set of ideal integers. But in computing it is not always the case i.e. (a+b)+c =/= a+(b+c) always because a/b/c are constrained/partial finite sets (i.e. int8/int16/int32 etc.) and thus the axiom of associativity will fail when for example, we take boundary values for a/b and a negative value for c (due to overflow/underflow). Thus any proof which uses the axiom of associativity for signed integers in a computer can never be as absolute and general as its counterpart in pure mathematics i.e. everything is Partial. In general, mathematics uses exact Analytical Techniques while computers use approximate Numerical Techniques to solve a problem which is reflected in the nature of their proofs.

Coming to DbC, since it is based on Hoare Logic (i.e. an algebra with axioms/inference rules), a Program is written as a series of Preconditions/Postconditions/Invariants with the Programmer acting as the Proof deriver. Thus if a series of pre/post/inv holds at a certain stage in the program (i.e. proof) the next post will hold (barring external cataclysms). The fact that the proof obligation is discharged dynamically at runtime is immaterial. But we may not want that in certain categories of real world programs since the question of what to do when the proof obligation is not met at runtime becomes a problem; Do we abort/Do we rollback to older known state etc. For a CRUD app we can abort and have the user restart but for a heart pacemaker app we don't want that. In the latter case since it is a closed system with well defined inputs/outputs we can map DbC to VDbC and then prove it through a verifier statically thus guaranteeing invalid states can never arise at runtime. But note that this is merely an incidental distinction due to the needs of the real world but the essential DbC guarantees remain the same.

It should now be clear that when you map concepts from mathematical to computing domain you need to understand how the same names like "Integer", "Set/Type", "Algebra", "Axiom", "Proof" map from one to the other (though not exactly) and how you can leverage their isomorphism to use symbolic Mathematics effectively in Programming while at the same time keeping in mind their differences due to real world computation constraints and limits.

References:

1) Mathematical Proof - https://en.wikipedia.org/wiki/Mathematical_proof

2) Computer-assisted Proof - https://en.wikipedia.org/wiki/Computer-assisted_proof In particular; see the "Philosophical Objections" section.

3) See also the book From Mathematics to Generic Programming by Alexander Stepanov and Daniel Rose to get an idea of how to map between mathematics and programming.