4 ms·

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

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 https://en.wikipedia.org/wiki/Mathematical_proof 2) Computer-assisted Proof - https://en.wikipedia.org/wiki/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.

rramadass 1y ago
Correction: In the 4th para above replace set N (set of natural numbers) with set Z (set of all positive and negative integers).
- MaxBarraclough 1y ago
  Don't forget zero!
  - rramadass 1y ago
    The set Z includes zero. Only when annotated eg. Z+, Z* etc. (often differently by different authors) are various subsets denoted.
    - MaxBarraclough 1y ago
      I'm aware ℤ includes zero, your definition set of all positive and negative integers excludes zero.
      - rramadass 1y ago
        That wasn't a definition but a comment since zero is implicit in Z unless stated otherwise.
MaxBarraclough 1y ago
> 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"). A proof of a program's correctness is mathematical in nature, it doesn't stand apart in some distinct non-mathematical realm. (Whether we call it computer science is of little consequence here.) The tools for generating such proofs tend to use SMT solvers. It's true that C's int type, for instance, does not correspond to the mathematical integers, despite the name. It has its own arithmetic rules. So what? It's still mathematical in nature. I think this is really a disagreement on phraseology though, nothing deeper. > 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. Programming languages can be modelled mathematically. Programs can be modelled mathematically. That's much of the point of formal methods. Real computers are finite state machines. So what? > 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 Modular arithmetic is mathematics, just as arithmetic over integers is mathematics. Formal analysis of floating-point arithmetic, or of C-style signed integer arithmetic, may be of less interest to pure mathematicians, but both can be (and have been) analysed with proper mathematical rigour. If someone really mistakes C's int type for the mathematical integers, or the float type for the reals, then they don't understand the first thing about programming. > 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. Sometimes we need to approximate the reals, sure, but there's nothing approximate about, say, mergesort. Similarly a proof of its correctness (whether in the abstract, or of a particular implementation in a programming language) isn't in any way approximate. > 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. As I understand it, in typical design-by-contract software development, there is no formal proving of anything, there's just runtime checking. It's possible to mistakenly believe we've come up with a model that is guaranteed to always preserve its postconditions and invariants. A decent introductory course on formal methods allows students to discover this for themselves, perhaps using Z Notation [0] or one of its derivatives. There's no substitute for proving your model correct. If your starting point really is a proper formal model with a proof of correctness, what you're doing isn't typical design-by-contract software development. > 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). We only know that's the case if we've formally proven that the program is correct. If you're doing runtime checking, it's presumably because you don't know whether the program always does as you hope in all possible states. > 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 [...] 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's not mere detail, it's an entirely different software engineering outcome. As you've just acknowledged, proving the absence of bugs from a codebase may be of life-and-death practical importance, and typically this cannot be achieved using runtime checks. A proof of correctness is a powerful assurance to have, and the tools needed to deliver it are radically different from runtime checks. It's in no way incidental, it's a whole different game. Even if you were able to test your program on all possible inputs, which you can't, you still probably haven't achieved the equivalent of a formal proof of correctness. There are plenty of issues that runtime assertions are likely unable to provide assurances for. Does the code have a subtle concurrency bug, or read-before-write bug, or some other form of nondeterministic behaviour, such that it might have failed to arrive at the correct outputs, but we just got lucky this time? Absence of undefined behaviour? Absence of sensitivity to platform-specific or implementation-defined behaviours or aspects of the programming language, such as the maximum value that can be held in an unsigned int? On the plus side, many of those issues can be mitigated by a well-designed programming language, or by compiler-generated runtime checks. The SPARK Ada language closes the door of many of them, for instance, whereas in C those sorts of issues are pervasive. More generally, testing and runtime checking are able to discover bugs, but are typically incapable of proving the absence of bugs. This is much of the motivation for formal methods in the first place. > 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 Again I don't think it's helpful to phrase it as if there are 2 worlds here, one mathematical and one not. Program behaviour can be modelled mathematically. It's not math-vs-programming, it's just a matter of applying the correct math. I'm not sure it's quite right to call it isomorphism, on account of computers being finite state machines. As you indicated earlier, computers can, roughly speaking, only cope with a subset of reality. [0] https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation

rramadass 1y ago

Correction: In the 4th para above replace set N (set of natural numbers) with set Z (set of all positive and negative integers).

MaxBarraclough 1y ago
Don't forget zero!
- rramadass 1y ago
  The set Z includes zero. Only when annotated eg. Z+, Z* etc. (often differently by different authors) are various subsets denoted.
  - MaxBarraclough 1y ago
    I'm aware ℤ includes zero, your definition set of all positive and negative integers excludes zero.
    - rramadass 1y ago
      That wasn't a definition but a comment since zero is implicit in Z unless stated otherwise.

MaxBarraclough 1y ago

> 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"). A proof of a program's correctness is mathematical in nature, it doesn't stand apart in some distinct non-mathematical realm. (Whether we call it computer science is of little consequence here.) The tools for generating such proofs tend to use SMT solvers. It's true that C's int type, for instance, does not correspond to the mathematical integers, despite the name. It has its own arithmetic rules. So what? It's still mathematical in nature. I think this is really a disagreement on phraseology though, nothing deeper. > 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. Programming languages can be modelled mathematically. Programs can be modelled mathematically. That's much of the point of formal methods. Real computers are finite state machines. So what? > 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 Modular arithmetic is mathematics, just as arithmetic over integers is mathematics. Formal analysis of floating-point arithmetic, or of C-style signed integer arithmetic, may be of less interest to pure mathematicians, but both can be (and have been) analysed with proper mathematical rigour. If someone really mistakes C's int type for the mathematical integers, or the float type for the reals, then they don't understand the first thing about programming. > 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. Sometimes we need to approximate the reals, sure, but there's nothing approximate about, say, mergesort. Similarly a proof of its correctness (whether in the abstract, or of a particular implementation in a programming language) isn't in any way approximate. > 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. As I understand it, in typical design-by-contract software development, there is no formal proving of anything, there's just runtime checking. It's possible to mistakenly believe we've come up with a model that is guaranteed to always preserve its postconditions and invariants. A decent introductory course on formal methods allows students to discover this for themselves, perhaps using Z Notation [0] or one of its derivatives. There's no substitute for proving your model correct. If your starting point really is a proper formal model with a proof of correctness, what you're doing isn't typical design-by-contract software development. > 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). We only know that's the case if we've formally proven that the program is correct. If you're doing runtime checking, it's presumably because you don't know whether the program always does as you hope in all possible states. > 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 [...] 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's not mere detail, it's an entirely different software engineering outcome. As you've just acknowledged, proving the absence of bugs from a codebase may be of life-and-death practical importance, and typically this cannot be achieved using runtime checks. A proof of correctness is a powerful assurance to have, and the tools needed to deliver it are radically different from runtime checks. It's in no way incidental, it's a whole different game. Even if you were able to test your program on all possible inputs, which you can't, you still probably haven't achieved the equivalent of a formal proof of correctness. There are plenty of issues that runtime assertions are likely unable to provide assurances for. Does the code have a subtle concurrency bug, or read-before-write bug, or some other form of nondeterministic behaviour, such that it might have failed to arrive at the correct outputs, but we just got lucky this time? Absence of undefined behaviour? Absence of sensitivity to platform-specific or implementation-defined behaviours or aspects of the programming language, such as the maximum value that can be held in an unsigned int? On the plus side, many of those issues can be mitigated by a well-designed programming language, or by compiler-generated runtime checks. The SPARK Ada language closes the door of many of them, for instance, whereas in C those sorts of issues are pervasive. More generally, testing and runtime checking are able to discover bugs, but are typically incapable of proving the absence of bugs. This is much of the motivation for formal methods in the first place. > 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 Again I don't think it's helpful to phrase it as if there are 2 worlds here, one mathematical and one not. Program behaviour can be modelled mathematically. It's not math-vs-programming, it's just a matter of applying the correct math. I'm not sure it's quite right to call it isomorphism, on account of computers being finite state machines. As you indicated earlier, computers can, roughly speaking, only cope with a subset of reality. [0] https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation