by rramadass | 2025-08-04 06:15:45+00:00
You have conveniently skipped the "Philosophical Objections" section in Wikipedia which i had pointed out and which would have given you some hints as to what i am saying.

> A proof of a program's correctness is mathematical in nature, it doesn't stand apart in some distinct non-mathematical realm ... I think this is really a disagreement on phraseology though, nothing deeper.

It is mathematical in nature but if the objects it deals with do not obey the axioms and/or the axioms are inconsistent the whole edifice falls. You can provide a perfectly "valid" proof but starting with wrong/inconsistent axioms. In computing since everything is a series of calculations it becomes quite important to make sure that you can carry-over the axioms in an algebra "as is" from pure mathematics to programming. In the example that i gave, the C language gives you multiple sets (aka types) of integers (i.e. cartesian product of {signed, unsigned} X {8, 16, 32, 64}) which are all subsets of the mathematical structure Z. You can distribute these types across the variables a/b/c in the expression in many different orders each of which have to be proven separately for the axiom of associativity to hold generally.

> 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?

Mathematics is static/declarative while Computing has both static/structural and dynamic/behavioural aspects both of which are amenable to mathematics but differently. This is the fundamental difference. It is also the reason so much of real world software is pretty good and correct in spite of not using any formal methods whatsoever. A "Proof" is simply a logical argument from {Premises} -> {Conclusion} whether done informally or formally. When we write a program we are the proof deriver logically moving from statement to statement to produce the desired result. This is "proof by construction" where we show that the final product (i.e. the program) meets the desired properties. By using Defensive Programming and Testing techniques we then "prove" at runtime that the properties hold. DbC is a more formal method of doing the same. TDD can also be considered as belonging to the same category.

> As I understand it, in typical design-by-contract software development, there is no formal proving of anything, there's just runtime checking ... 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.

This is your fundamental misunderstanding. By "Formal" you are only looking at static verification of the program and ignoring all runtime aspects. DbC is formal verification at runtime of a proof you have hand derived statically using set theory/predicate logic as you write the program. It does not make it any less than other formal methods done statically (hence the easy mapping done to VDbC). It is the real world needs of the system which decides what is acceptable as pointed out previously.

There is also a movement towards "lightweight formal methods" where partial specification, partial analysis, partial modeling and partial proofs are deemed acceptable because of the value they provide.

> It's not mere detail, it's an entirely different software engineering outcome. ... 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.

No amount of Formal Methods application can help you against something going wrong in the environment (hence my use of the word cataclysm) and which directly affects the system eg. a EMP pulse corrupting memory, hardware failures etc. We mitigate against this using Redundancy and Fault-Tolerance techniques. Because in computing we have static and dynamic aspects we need to consider both as the field of use for Formal (and other) Methods.

> Again I don't think it's helpful to phrase it as if there are 2 worlds here, one mathematical and one not.

There absolutely is. It is the definition of Ideal vs. Real Worlds. In Computing you have the limitations of finite time, finite steps, finite precision, finite error/accuracy etc. It changes the very nature of how you would map mathematics to reality.

References:

1) Proof by Construction - https://en.wikipedia.org/wiki/Mathematical_proof#Proof_by_co...

2) Stackexchange and HN discussion Why is writing mathematical proofs more fault-proof than writing code? - https://news.ycombinator.com/item?id=16045581

3) When is a computer proof a proof? - https://lawrencecpaulson.github.io/2023/08/09/computer_proof...

4) The Central Dogma of Mathematical Formalism - https://siliconreckoner.substack.com/p/the-central-dogma-of-...

5) Lightweight Formal Methods - https://people.csail.mit.edu/dnj/publications/ieee96-roundta...