> the average software engineer needs approximately none of that.
Not true. He/She doesn't need to know all of it nor in depth but a conceptual understanding is very much needed to write "correct" (w.r.t. a specification) code. We Humans are natural algorithmic problem solvers and hence can always muddle our way through to a ad-hoc solution for a given problem. Obviously, a lot depends on the intelligence of the individual here. What Mathematics gives you is a structure and concepts to systematize our thinking and rigorously apply it so that problem solving becomes more mechanical. Thus you learn to specify the problem rigorously using mathematical concepts and then use mathematical logic to derive a "Program" satisfying those requirements.
At the very least a knowledge of Set Theory, Logic and Relational Algebra goes a long way towards understanding the mapping from Mathematics to Computer Programming.
The following books are helpful here;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke. A very nice overview and wide coverage of needed basic mathematics.
2) Understanding Formal Methods by Jean-Francois Monin. A fire-hose overview of mathematical models and tools implementing those models.
> At the very least a knowledge of Set Theory, Logic and Relational Algebra goes a long way towards understanding the mapping from Mathematics to Computer Programming.
I know all these from university, but I did programming and SQL before that without any issues. Learning these mathematical details seemed really not useful in practice, at least for me.
Of course, coming up with something like SQL in the first place requires a lot of theoretical mathematics (set theory, relational algebra), but as someone who only uses those systems, like 99% of software engineers, understanding the mathematical theory here doesn't seem very helpful.
I am afraid you have not really understood the mathematical theory and its mapping to programming. Relational Algebra doesn't just mean RDBMS/SQL but is a general algebra where algebraic Operations are defined over mathematical Relations i.e. over a Cartesian Product of one or more Sets.
As a first approximation; a) Type = Set b) Function = subset of Relation (i.e. set of Tuples) obtained from Cartesian Product of {input type set X output type set} c) Logical conditions define new relational sets where its members have a ordering relation d) A Program is a series of functions which prune and transform the tuples from the above cartesian product.
Well, I'm familiar with model theory and Church's simple theory of types, but I don't think things like that are useful in practice. Perhaps the concept of currying would be an exception, if I were a Haskell programmer.
I am not sure that you have really understood the topics you have named. All high-level programming languages give you a set of fundamental types and the ability to construct user-defined types. Currying is not an exception but falls under the same model if one considers it as a Relation between "sets of functions". Also by Curry-Howard correspondence you have "formula/proposition = type" and "proof = function". So you have a direct mapping between Sets/Relations/Logic in Mathematics and Types/Logic in a Program.
A Program then becomes a trajectory enforced using predicate logic through a state space obtained from the cartesian product of all the types in the program.
You are using all of the above whether you know it or not when programming in a high-level language. The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification).
> You are using all of the above whether you know it or not when programming in a high-level language.
Exactly. The average programmer doesn't have to know the math behind things like types to use them.
> The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification).
I don't think the average software engineer does that or would benefit from doing it. I certainly don't.
> I don't think the average software engineer does that or would benefit from doing it. I certainly don't.
Again; you are drawing the wrong conclusions and projecting your own ignorance on others.
To give a simple analogy; anybody can swing a baseball bat at a ball. But that won't make him a notable player. To become a superlative player one needs to understand body dynamics and train scientifically. In a similar vein, anybody can muddle through and come up with a Program. But more often than not, it will be error-prone and bug-ridden not to mention hard to extend and maintain. Given the importance of Software to our modern society this is not what we want. A little bit of knowledge of Mathematics behind Programming gives you orders of magnitude return in software quality which is absolutely worthwhile.
There is nothing to debate/argue here but merely pointing out the application of scientific method to software engineering.
> Again; you are drawing the wrong conclusions and projecting your own ignorance on others.
I reject your accusation. It's more likely that you are the one who is projecting, namely your ignorance of what the average software engineer is doing.
Your opinion has zero basis in facts and betrays some serious ignorance of Scientific Method. No educated person can deny the importance of Mathematics to our technologically advanced society today. Computer Science is a subfield of Mathematics and Computer Programming is the application of principles and concepts studied therein.
As mentioned earlier, the point of studying Mathematics for Computer Science is to make your "average software engineer" better and more productive than he/she was in the past.
> The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification).
At the risk of nitpicking:
Certainly it's a benefit to structure and understand code such that you can reason about it effectively, but prove goes too far. Almost no real code is proven correct, the ergonomics of formal methods are still far too poor for that.
It depends; the "proving" can be done at a gross high level function or fine grained at statement level. Thus in the former case one could use Meyer's Design-by-Contract (aka DbC) while in the latter case one might choose to follow a detailed Dijkstra methodology. For both of the above you don't need any special tools (eg. Z/VDM/TLA+/Coq/Lean etc.) but merely the knowledge to learn to think about a Program using Mathematical Concepts. For most "ordinary" software, DbC would be enough while for critical software one might want to go with the whole nine yards using chosen methodologies/tools. Note that usage of the methodologies/tools themselves require a knowledge of the above-mentioned Mathematics.
The point was that a knowledge of the requisite Mathematics gives you a very powerful way of viewing Programs and then you get to choose how to map/implement it using any number of tools and based on the needs of the software.
Design-by-contract typically refers to runtime checking of invariants, which is not the equivalent of formal verification. It should not be referred to as proving correctness. It doesn't do so.
If you want to prove your program's correctness, that's the domain of formal methods, essentially by definition.
This argument has been made before and that is why i said it depends and put "proving" within quotes. It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject (as my comments to user cubefox shows).
A Formal Method defined broadly is the application of Mathematical Concepts/Models and Logic to the specification/implementation/verification of Computer Programs.
DbC is based on Hoare Logic where you try to "prove" the program intellectually and not necessarily tool driven. This was somewhat mechanized (though still a intellectual pursuit) by Dijkstra's technique of deriving weakest-preconditions. Because the whole process can be quite tedious, laborious and rather complex, automatic theorem prover tools were invented to do the job for you. This has resulted in the unfortunate status quo where Formal Specification/Verification have become identified with the use of tools and not the Mathematics behind them. Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools.
DbC can be considered a lightweight Formal Method with aspects of both Specification and Verification included. The Programmer plays the role of "theorem prover" when using DbC. However tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs. See for example https://www.eschertech.com/products/verified_dbc.php. Also Eiffel (quintessential DbC language) can be converted using AutoProof to a form which can be proven by Boogie verifier.
> that is why i said it depends and put "proving" within quotes
I feel I need to insist on this point: a design-by-contract methodology using
runtime checking may be an effective means of improving software quality, but it
certainly isn't proving the correctness of a program. Using the word 'prove'
here is just plain wrong. Putting it in quotation marks doesn't help. It simply
does not constitute a proof.
> It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject
I'm not insisting on a narrow understanding of formal methods, I'm insisting on
proper use of established terminology.
I'm all for practical methodologies that benefit software quality without paying
the enormous costs of fully applying formal methods. Design-by-contract with
runtime checking seems like a reasonable approach. (Static typing is another.
Effect-oriented programming might be another.) My point was just about the
proper use of the word proof.
> Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools.
A program is proven correct only when the proof is absolute, which implies
fine-grained. I'm not opposed to the use of partial proofs or 'good enough'
proof-sketches, both of which could be useful in producing high-quality software
in the real world, but we should be clear in how we refer to them.
I'm not sure about the idea of proving correctness by hand, though. Manually
applying a formal model of a real programming language sounds unworkable. If
code is well structured, it should be possible for the programmer to reason
about it somewhat precisely, like a proof-sketch, but that's not a proof of
correctness.
> The Programmer plays the role of "theorem prover" when using DbC
I don't find this convincing. There's nothing stopping the programmer from
failing to notice some error. If you aren't actually doing a proof, just say so.
There is no stand-in.
> tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs.
Right, I hinted at this in my previous comment. SPARK Ada does this. In that
case, correctness properties of the program are indeed formally proven. That's a
quite different methodology to design-by-contract with runtime checking though,
to the point that it almost seems unhelpful to refer to them both by the same
name. I've had to be careful to explicitly state design-by-contract using
runtime checking this whole time.
The deeper distinction here is between testing and formal proof, and
design-by-contract can in principle refer to either.
> here is a case study Design by contract formal verification for automotive embedded software robustness
I have used SPARK Ada myself on a couple of security focused products developed by a team of 10-15 developers. For a long time, SPARK has made use of formal methods practical for real-world software. Effective use does require learning and commitment, but that's within reason. By the time the projects were nearly done, I felt that the SPARK findings always turned out to be correct and that any remaining problems could be traced back to poor or missing requirements, not the implementation itself.
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.
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.
> 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.
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.
> You have conveniently skipped the "Philosophical Objections" section in Wikipedia
As far as I can see, that Wikipedia section doesn't connect to anything we've discussed.
We haven't discussed the impracticality of human verification of machine-generated proofs of properties of complex programs or models. We haven't discussed the possibility of bugs in verifier software.
> 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.
Sure, but you seem to be stressing the risk of misapplication of mathematical axioms such as those of integer arithmetic, to contexts where they do not hold, such as arithmetic over int in the C language. As I've stated, formal methods are able to accommodate that kind of thing. We're both already aware of this.
You can formally reason about a program written in C, but naturally you need to be keenly aware of the way C code behaves, i.e. the way the C language is defined. You need to model C's behaviour mathematically. As you've hinted at, you need to account for the way unsigned integer arithmetic overflow is defined as wrapping, whereas signed integer arithmetic overflow causes undefined behaviour. The formal model of the source programming language essentially forms a set of axioms. Existing tools already do this.
> 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.
I'm not clear what software development methodology you have in mind here. It sounds like you're describing a formal methodology. It certainly doesn't describe ordinary day-to-day programming.
> By using Defensive Programming and Testing techniques we then "prove" at runtime that the properties hold.
These do not constitute a proof over the program.
> 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.
No, again, that isn't proof in the sense of serious formal reasoning about a program. I guess it's a proof in the trivial sense, courtesy of the Curry–Howard correspondence, but I don't think that's what you're referring to.
In my prior comment I gave a list of reasons why runtime checking doesn't even necessarily prove that the program correctly implements a correspondence from the one particular input state to the one particular output state, as there's plenty of opportunity for the program to accidentally contain some form of nondeterminism such that it only happened to derive the correct output state when it actually ran. Program behaviour might be correct by coincidence, rather than correct by construction.
Consider this C fragment by way of a concrete example. I'll use undefined behaviour as the root cause of troublesome nondeterminism, but as I mentioned in my earlier comment, another would be race-conditions.
int i = 1 / 0;
int k = 42;
i = k;
At the end of this sequence, what state is our program in, reasoning by following the definition of the C programming language as carefully as possible and making no assumptions about the specific target platform?
Incorrect answer: i and k both hold 42, and execution can now continue. Variable i was briefly assigned a nonsense value by performing division by zero, but the last assignment renders this inconsequential.
Correct answer: undefined behaviour has been invoked in the first statement. This being the case, the program's behaviour is not constrained by the C standard, so roughly speaking, anything can happen. On some platforms it may be that i and k both hold 42, and that execution can now continue without issue, but neither is guaranteed by the C language. Nothing that occurs subsequently in the program's execution can reverse the fact that undefined behaviour has been invoked.
This is of course a trivial contrived example that's impossible to miss, but in practice, plenty of C programs accidentally rely on implementation-defined behaviour, and many accidentally invoke undefined behaviour, according to the C standard.
Putting lots of assertions into your code isn't an effective way of catching that kind of issue in practice. If it were, we wouldn't have so many security issues arising from memory-management bugs.
Even if all that weren't the case though, runtime testing still can't exhaustively cover all cases, whereas formal proofs can.
> TDD can also be considered as belonging to the same category.
No, that's really quite absurd. Try arguing to a formal methods research group that TDD is tantamount to formal verification. They'll laugh you out of the room.
> DbC is formal verification at runtime of a proof you have hand derived statically using set theory/predicate logic as you write the program.
For the reasons I gave above, it does not even definitively demonstrate the correctness of the code for a given input state, let alone in general.
Most people doing 'design by contract' are not starting out with a formal model expressed in set theory. I think you should find another term to refer to the methodology you have in mind here, it's confusing to refer to this as 'design by contract'.
You generally can't practically hand-derive proofs of properties of a large program or formal model, that's why computerised solutions are used.
> 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.
Sure, like I said earlier: I'm not opposed to the use of partial proofs or 'good enough' proof-sketches, both of which could be useful in producing high-quality software in the real world, but we should be clear in how we refer to them.
Something I should have added at the time: when using a formal software development methodology, it's possible, and likely necessary for practical reasons, to prove only a subset of the properties that constitute the program's correctness.
> No amount of Formal Methods application can help you against something going wrong in the environment
Of course.
> In Computing you have the limitations of finite time, finite steps, finite precision, finite error/accuracy etc.
Right, but do any of these defy mathematical modelling?
Limitations of that sort might make programs mathematically uninteresting, but that's almost the opposite of them being fundamentally irreducible to mathematics.
> As far as I can see, that Wikipedia section doesn't connect to anything we've discussed....
It is directly relevant to your misunderstanding of terms like "Proof" and "Formal". That and the various other references i had provided should give you enough information to update your knowledge. It is only when you start thinking at a meta-level (i.e. philosophical level) that you can understand them.
> Sure, but you seem to be stressing the risk of misapplication of mathematical axioms such as those of integer arithmetic, to contexts where they do not hold, such as arithmetic over int in the C language. ... The formal model of the source programming language essentially forms a set of axioms. Existing tools already do this.
Again, you have not understood my example at all. It has nothing to do with the C language but everything to do with axioms in mathematics mapped to any language. The fact that subsets of integer are represented as finite overlapping sets means their order of application in an expression (i.e. intersection) becomes significant and each order has to be proved separately which is not the case in mathematics.
> I'm not clear what software development methodology you have in mind here. It sounds like you're describing a formal methodology. It certainly doesn't describe ordinary day-to-day programming.
This is just normal programming where you explicitly think about the transformations of the state space where you execute the code mentally while moving from statement to statement. People do this naturally as they devise a algorithm. They just need to be taught how to formalize this using some rigorous notation after being shown the mapping to mathematical concepts.
> These do not constitute a proof over the program ... No, again, that isn't proof in the sense of serious formal reasoning about a program. I guess it's a proof in the trivial sense, courtesy of the Curry–Howard correspondence, but I don't think that's what you're referring to.
That is exactly what i am referring to. It is "proof in the trivial sense" and hence my mentioning defensive programming and testing techniques to go with the above. All programmers do this in the course of their everyday work and this is the main reason there is so much good software out there in spite of not using any formal methods. Note that the "correctness" of the final product depends to a large extent on the expertise/knowledge of the programmer.
> In my prior comment I gave a list of reasons why runtime checking doesn't even necessarily prove that the program correctly implements a correspondence from the one particular input state to the one particular output state, as there's plenty of opportunity for the program to accidentally contain some form of nondeterminism such that it only happened to derive the correct output state when it actually ran. Program behaviour might be correct by coincidence, rather than correct by construction.
I had already pointed out the static/structural and dynamic/behavioural aspects of a program and how you can map between and use the two. You can give specifications statically (eg. Typing) but verify them either statically (eg. total function from one type to another) or at runtime (eg. partial function from one type to another).
> Consider this C fragment by way of a concrete example. ... This is of course a trivial contrived example that's impossible to miss, but in practice, plenty of C programs accidentally rely on implementation-defined behaviour, and many accidentally invoke undefined behaviour, according to the C standard.
This is not directly relevant here.
> Putting lots of assertions into your code isn't an effective way of catching that kind of issue in practice. If it were, we wouldn't have so many security issues arising from memory-management bugs. Even if all that weren't the case though, runtime testing still can't exhaustively cover all cases, whereas formal proofs can.
Again, your understanding is simplistic and incomplete. C.A.R.Hoare wrote a retrospective paper to his classic paper on Hoare Logic after 30 years which clarifies your misunderstanding Retrospective: An Axiomatic Basis For Computer Programming - https://cacm.acm.org/opinion/retrospective-an-axiomatic-basi...
Excerpts;
My basic mistake was to set up proof in opposition to testing, where in fact both of them are valuable and mutually supportive ways of accumulating evidence of the correctness and serviceability of programs. As in other branches of engineering, it is the responsibility of the individual software engineer to use all available and practicable methods, in a combination adapted to the needs of a particular project, product, client, or environment.
I was surprised to discover that assertions, sprinkled more or less liberally in the program text, were used in development practice, not to prove correctness of programs, but rather to help detect and diagnose programming errors. They are evaluated at runtime during overnight tests, and indicate the occurrence of any error as close as possible to the place in the program where it actually occurred. The more expensive assertions were removed from customer code before delivery. More recently, the use of assertions as contracts between one module of program and another has been incorporated in Microsoft implementations of standard programming languages. This is just one example of the use of formal methods in debugging, long before it becomes possible to use them in proof of correctness.
> No, that's really quite absurd. Try arguing to a formal methods research group that TDD is tantamount to formal verification. They'll laugh you out of the room.
No, a person who is educated in Formal Methods would know exactly in what sense i am using TDD as a formal method. Hoare in the above article gives you a pointer for edification.
> For the reasons I gave above, it does not even definitively demonstrate the correctness of the code for a given input state, let alone in general. Most people doing 'design by contract' are not starting out with a formal model expressed in set theory. I think you should find another term to refer to the methodology you have in mind here, it's confusing to refer to this as 'design by contract'. You generally can't practically hand-derive proofs of properties of a large program or formal model, that's why computerised solutions are used.
You have failed to understand what i have already written earlier. DbC is based on Hoare Logic which is axiomatic formal system using set theory/predicate logic. So when a programmer devises the contracts (preconditions/postconditions/invariants) in DbC he is asserting on state space which can be verified at runtime or statically by generating verification conditions which are fed to a prover.
> Sure, like I said earlier: I'm not opposed to the use of partial proofs or 'good enough' proof-sketches, both of which could be useful in producing high-quality software in the real world, but we should be clear in how we refer to them. Something I should have added at the time: when using a formal software development methodology, it's possible, and likely necessary for practical reasons, to prove only a subset of the properties that constitute the program's correctness.
I had already pointed out that you need to both define and understand Formal Methods broadly for effective usage. The fundamental idea is what is known as "Formal Methods Thinking" defined from basic to advanced where at each level you learn to apply formal methods appropriate to your understanding/knowledge at that level. Read this excellent and highly practical paper which will clarify what i have been saying all along in this discussion; On Formal Methods Thinking in Computer Science Education - https://dl.acm.org/doi/10.1145/3670419
> Right, but do any of these defy mathematical modelling? Limitations of that sort might make programs mathematically uninteresting, but that's almost the opposite of them being fundamentally irreducible to mathematics.
They both limit the applicability of mathematical models as-is and at the same time give you greater opportunities to extend the mathematics to encompass different sorts of behaviours.
Finally, to bring this to a conclusion, read Industrial-Strength Formal Methods in Practice by Hinchey and Bowen for actual case studies. In one project for a control system, a complete specification is done using Z notation which is then mapped directly by hand to C code. The proof is done informally with actual model checking/theorem proving only done for a very small piece of the system.
Not true. He/She doesn't need to know all of it nor in depth but a conceptual understanding is very much needed to write "correct" (w.r.t. a specification) code. We Humans are natural algorithmic problem solvers and hence can always muddle our way through to a ad-hoc solution for a given problem. Obviously, a lot depends on the intelligence of the individual here. What Mathematics gives you is a structure and concepts to systematize our thinking and rigorously apply it so that problem solving becomes more mechanical. Thus you learn to specify the problem rigorously using mathematical concepts and then use mathematical logic to derive a "Program" satisfying those requirements.
At the very least a knowledge of Set Theory, Logic and Relational Algebra goes a long way towards understanding the mapping from Mathematics to Computer Programming.
The following books are helpful here;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke. A very nice overview and wide coverage of needed basic mathematics.
2) Understanding Formal Methods by Jean-Francois Monin. A fire-hose overview of mathematical models and tools implementing those models.