In theory, your software itself provides the proof that it does what it claims. The proof would directly link to unit tests or integration tests at the meta level.
Arguably, software engineering does this much more exhaustively then any other engineering field... To very varying quality output, from masterpieces like SQLite to your average B2B artifact which barely works despite having 99% coverage.
Tests are a basis for every engineering discipline. In software we have the luxury of being able to test each delivered project. Other engineered projects often only have their components tested, and then need to rely on calculations to determine the end result.
Tests proof that something can handle the exact scenario that we're testing. The forces on a software system are just different and in some ways less predictable than for e.g. a building. But in software the consequences of failure are often less catastrophic[1] and it's a lot cheaper to run a battery of tests.
[1] And if they are not less catastrophic than a collapsing building, you'd better test it far more extensively than an average system. That's engineering too, making a trade-off between the costs of failure and the cost of preventing failure.
Proof by exhaustion, also known as proof by cases, proof by case analysis, complete induction or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases or sets of equivalent cases, and where each type of case is checked to see if the proposition in question holds.
It is only fitting if you think of providing the proof as a push button technology. That makes as much sense as thinking of providing the software itself as a push button technology.
It has nothing to do with the proof as a push button technology.
Adding annotations to the code for example is not a workaround for the halting problem.
(Working with a subset that's not-turing complete is, but that doesn't cover the general case the parent calls for, and is not practical with current software development languages and practices).
Not sure if we are talking about the same thing. If you know why your software is correct, you can write that down as a proof (if you have a language which allows you to do that). If you don't know why your software is correct, well, maybe you should not ship it, because maybe it isn't correct.
So yes, it is all about push button technology here. If you are willing to put in the work to write down the proof yourself, instead of expecting a magical entity to generate it for you, then it is possible. All the halting problem says is that there is no such magical entity. You will need to know why your software is correct.
Exactly. In practice you always want each loop iteration to perform some action that brings you closer to some desired end state. That loop invariant + some notion of getting closer to the end is usually the proof you need to prove termination. A loop where you don't have these things is almost certainly a bug.
The vast majority of loops iterate over some finite collection of elements and are thus guaranteed to terminate. Tricky cases are stuff like "I will repeat this operation until the output stops changing".
>Exactly. In practice you always want each loop iteration to perform some action that brings you closer to some desired end state. That loop invariant + some notion of getting closer to the end is usually the proof you need to prove termination.
If you're making Space Shuttle software from scratch yes. In practice for 99% of current mainstream development you depend on piles upon piles of dependencies, which might or might not check those loop invariants correctly, or might have a (trivial to add) endless blocking timeout, a deadlock, and many other wonderful things.
Usually they're not even set in stone, you'll update to the next version, and if they introduced such an issue, there's lots of fun to be had.
Nobody doubted you can have formal proofs for algorithms, or checked software in certain conditions and for certain controlled environments (e.g. using MISRA C and such) (in fact, I support this in a comment elsewhere in this thread).
The objection is to the idea that this is applicable (or trivially applicable, and we just aren't doing it out of laziness or something) to regular software development.
The halting problem is not an actual issue. It’s a darling of computer science classes, but is you need to prove that your program halts, it’s not that hard to write it in a language subset that is not turing-complete.
The calculations you do to make sure that the bridge doesn’t collapse also require that the steel matched whatever properties your formula assumes. That doesn’t make the calculations useless.
Continuing the stream of inputs holds no meaning once you've tested every possible permutation (branch coverage) beyond checking for memory leaks. Every software has a finite amount of states it can hold, most developers just erroneously expect some states to be unlikely or impossible to reach.
> If you manage to solve the halting problem first.
there is a large slice of algorithms, which are possible to prove that they are not affected by halting problem. I think having tooling for this slice of algorithms is already a big win.
I don't agree that that's exhaustive testing. Full branch test coverage etc., is normal and sensible and it's great, but that's very different from having a proof that given certain preconditions, you will have certain postconditions.
100% branch coverage means that you've fundamentally covered all potential states your software can enter.
What you're asking for is literally only possible in theory and entirely pointless in the context of reality, because you cannot guarantee that a device is available at runtime, invalidating any proof. The same applies to any engineering projects, software or otherwise
if (x > 0) {
/* code */
} else {
/* more code */
}
Branch coverage just means that all the lines above are executed in some test. That's fundamentally different from dealing with all the different values that `x` could take on at run time.
Given your example no software can ever handle this equation given infinite numbers, as all CPUs have a maximum number they can compare.
Just like you cannot prove that a bridge will be able to handle a given load. Engineering fundamentally can only make assurances within expectations. Your tests define these expectations, and by covering 100% branching coverage you've exhaustively explored all valid states your software can have.
Do note I'm talking about actual 100% branching coverage here, not just 100% coverage of your own code, ignoring libraries and runtimes you've imported. That's way harder then you seem to think and the reason why sqlite (the linked page) has so much more testing code then application code
I agree with the other commenter that his is not even remotely true... given something like
loop {
if (A) { ... }
if (B) { ... }
}
100% branch coverage means you've encountered both cases, but the loop could have encountered these in any number of ways specifically this branch could be encountered as either A && B both A && !B && B && !A, all of them exhaustively, and could even depend upon whether the order branches were taken matters.
I guess we're desperate to get to answer to the question of how dumb comment chains on this forum can get, and wherever everyone involved is either mentally or actually in the /r/im-12-and-this-is-smart phase.
Arguably, software engineering does this much more exhaustively then any other engineering field... To very varying quality output, from masterpieces like SQLite to your average B2B artifact which barely works despite having 99% coverage.