You are right that really verifying programs is prohibitively expensive and extensive. Most software projects cannot afford a full-blown verification.
However, if the engineers on the project know a thing or two about how to write code as if it would be verified, it makes the code much easier to read. In my experience, such code is often easy to look at and say "Oh, that's obviously correct".
Then one can verify the most critical parts of the program, and leave the rest to intuition.
I would of course not design a nuclear power plant or missile control system in that way, but for most projects, such an approach would be feasible.
It all boils down to a bit of structure in your code, really. And certifying engineers who can write proper code is a Good Thing.
Slashdot Mirror
You are right that really verifying programs is prohibitively expensive and extensive. Most software projects cannot afford a full-blown verification.
However, if the engineers on the project know a thing or two about how to write code as if it would be verified, it makes the code much easier to read. In my experience, such code is often easy to look at and say "Oh, that's obviously correct".
Then one can verify the most critical parts of the program, and leave the rest to intuition.
I would of course not design a nuclear power plant or missile control system in that way, but for most projects, such an approach would be feasible.
It all boils down to a bit of structure in your code, really. And certifying engineers who can write proper code is a Good Thing.
But then, what do I care what you 'merkins do.
--
--
I actually read that next part as
"This biweekly zine will help you know better."
Oh, well. Need more caffeine, I guess.