OSDev.org

Hi,

Love4Boobies wrote:Heh, my post got removed, probably because of the Spiderman image (seriously?). Anyway, I had mentioned to alexfru formal verification as a way to guarantee bug-free code, as long as the specification accurately describes the product you want to create but that it's more trouble than it's worth for most projects.

For people who aren't familiar with the steps needed for formal verification of software; it goes like this:

• start with a wrong design
• get the same small team of developers to implement the wrong design twice - once as normal code and again as the "formal specification", and maximise the chance of the same developers making the same mistakes in both versions
• use a buggy tool to "verify" that the bugs in the code actually do match the bugs in the formal specification
• claim that the resulting code was formally verified to mislead people into thinking the resulting software actually works even though you've know it doesn't; because you've already spent 2 years working on something that should've taken 1 year and you've realised that debugging the code, the formal specification and the tool used to verify is 3 times as hard as just debugging the code

Cheers,

Brendan

That's a gross exaggeration of the state of affairs.

Brendan wrote:

• start with a wrong design

That's unavoidable, unfortunately. It also applies to "legacy" software.

Brendan wrote:

• get the same small team of developers to implement the wrong design twice - once as normal code and again as the "formal specification", and maximise the chance of the same developers making the same mistakes in both versions
• use a buggy tool to "verify" that the bugs in the code actually do match the bugs in the formal specification

Actually, the modern way to do it is to generate the code directly from the formal specification. Regarding bugs, trusting theorem provers is not as insane as you make it out to be. For instance, it's almost certain that any non-verified hardware, operating system, and compiler has bugs, yet for the most part you trust their output; it would be insane to advocate writing machine code by hand because compilers are buggy (usually, in a way that won't even affect you), wouldn't it? At least their bugs are consistent and once removed, they disappear everywhere. You're a buggy compiler, too, and you can't be reliably debugged. The right way to think about it is not in terms of blind trust but in terms of degree of trust. After all, no interesting software can be proved consistent with certainty, as per Gödel's first incompleteness theorem from inside our universe.

Brendan wrote:

• claim that the resulting code was formally verified to mislead people into thinking the resulting software actually works even though you've know it doesn't; because you've already spent 2 years working on something that should've taken 1 year and you've realised that debugging the code, the formal specification and the tool used to verify is 3 times as hard as just debugging the code

It's obviously not the right approach to any project and I've admitted to that already. You've just picked a hypothetical project that suits your argument and than assumed formal verification for it so as to try to deny the validity of formal verification in general. Empirically, formally verified software is more trustworthy so I will have to call bias on your part.

Hi,

Love4Boobies wrote:That's a gross exaggeration of the state of affairs.

Love4Boobies wrote:Actually, the modern way to do it is to generate the code directly from the formal specification.

Awesome! In that case, everything I've ever written is formally verified (I write my formal specifications in languages like assembly and C).

Love4Boobies wrote:It's obviously not the right approach to any project and I've admitted to that already. You've just picked a hypothetical project that suits your argument and than assumed formal verification for it so as to try to deny the validity of formal verification in general. Empirically, formally verified software is more trustworthy so I will have to call bias on your part.

Empirically, when it's raining I'm almost always indoors, therefore the chance of rain decreases if I go outside.

The more you care about correctness (rather than budgets and release dates chosen by marketing people) the more trustworthy the code is going to be. People who care about correctness the most have the most trustworthy code (and are more likely to try formal verification, but that's just a coincidence).


Cheers,

Brendan

The difference is your formal specifications in assembly and C have to be manually checked for things like undefined behavior (or things that would be generated from UB in the case of assembly).

Brendan wrote:

Love4Boobies wrote:Actually, the modern way to do it is to generate the code directly from the formal specification.

Awesome! In that case, everything I've ever written is formally verified (I write my formal specifications in languages like assembly and C).

Indeed, code is a textual specification of software behavior and wrong specifications lead to wrong behavior just as proving the wrong thing leads to the wrong behavior. However, the point is that the proof statement is typically more concise than the proof object itself and you have the machine checking whether your proof is correct or not (in the computationally cheap cases, it might generate the proofs directly). So, for instance, if you're trying to sort a list in increasing order, you might have a proof statement that says that each element, except for the first is larger than the previous. The particular algorithm you implement depends on your proof, of course; after all, computation can be viewed from the perspectives of logic (proofs and propositions), languages (programs and types), and categories (mappings and structures) and there are correspondences between each.

Rusky wrote:The difference is your formal specifications in assembly and C have to be manually checked for things like undefined behavior (or things that would be generated from UB in the case of assembly).

The real problem is that his algorithms are not proved correct with respect to simple statements. The intricacies of any particular language are unimportant as far as this discussion goes. But, sure, for the cases where you can't tell at compile time, your only alternative to proofs would be detecting things at runtime and then reporting them for maintenance purposes. I just didn't get the part about assembly. Why does it matter if it contains code generated for UB? You want to avoid UB in your C code because relying on it is unportable but if you've got it in assembly form and it does what you want, you've already jumped that fence.

Indeed. I'm just appealing to Brendan's level of comprehension- proving higher level properties is of course the more important part.

I recommend this video introduction which shows the general principle and how little you have to trust compared to how much gets verified.