As far as I'm aware, unless your software is Hello World simple, the only way to make sure it's correct is to not write it in the first place.
After that point, everything is a compromise.
After that point, everything is a compromise.
Sometimes the spec is a bit wrong, like forgetting to be explicit in precisely how the system should crash on a certain unexpected input.
It is pretty much impossible to write meaningful tests that cover everything.
This is especially true, when you mix complex, asynchronous server interactions, with random-access UI.
Today, I am fixing a couple of bugs in an app that interacts with three different servers (all asynchronously, but some semi-synchronously. The timing diagram is a bit ... intense), and also allows the user to do things like switch contexts, while some part of the server interaction is still unresolved.
I write a bit about my approach to testing, here: https://littlegreenviper.com/miscellany/testing-harness-vs-u...
Wanted to let you know that the "Here is the Doxygen-generated documentation for the BADGER layer" link is broken on this page: https://littlegreenviper.com/miscellany/forensic-design-docu...
I'll look at that.
But, of course, this is why we use CI.
End even then only if you stick to English strig hello world.
I have had hello worlds fail, in other languages :)
It is some kind of logical fallacy - just because really smart people worked on something and dedicated their lives to it doesn't mean it is good or correct or that it works.
It was sold as the "rolls royce of testing" which I think overstated its capabilities and effectiveness.
Model checking can be pretty productive relatively speaking, however.
Of the remaining problems, the complete, formal specification would be larger, more complex, and more bug-ridden than the implementation. "Hey adwn, can you add a button to the GUI so the user can export the current dataset to a CSV file?" Maybe 20-50 lines of code, but a full specification would be a multi-year project – and it would be almost certainly wrong.
And even if they can, where does that formal spec come from? Sooner or later, it comes from some informal understanding of what's supposed to happen. Well, how do you check that the formal spec is correct? Because if you can't do that, all formal verification can do is tell you that your program correctly implemented the wrong thing.
And I don't think you can do that. First, I don't think you can go from informal to formal by formal means. Second, even if you can, you still can't verify the informal spec. So formal verification can only go so far.
I can recall several things that were bugs in the spec. Log4j is the most recent example. Heartbleed I think was a specification bug. Back in the day, a lot of computer viruses were helped on their way by bad ideas in the specification of Microsoft Outlook.