3 ms·

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

• MaxBarraclough 1y ago
  > 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.