> 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.
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.
I doubt that you really understand DbC so start with wikipedia (https://en.wikipedia.org/wiki/Design_by_contract) and then Meyer's OOSC2 (https://bertrandmeyer.com/oosc2/) for details. Finally, see Meyer's paper "Applying Design By Contract" (https://se.inf.ethz.ch/~meyer/publications/computer/contract...) for implementation advice.
> 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.