3 ms·

> They proved that it implements "the spec" perfectly, but to do that, you need a detailed spec with no abstractions. No you don't. > That means the spec cont

> They proved that it implements "the spec" perfectly, but to do that, you need a detailed spec with no abstractions. No you don't. > That means the spec contains just as much information as the code itself, which means the spec is just as complex as the code. No it doesn't. > Thus, the spec is just as vulnerable to hacks as any other work created by fallible humans. The spec can be smaller and more accessible than the code. > So essentially, proving that the code is a perfect implementation of the spec tells you nothing. It tells you that you can read the spec and know exactly what the code will do. For example it won't BSOD (unless someone was silly enough to put that in the spec). . I can have a function "int exp(int a, int b)", and a spec that says it returns "a^b" (or "a b" or however you want to write it), or throws a IntegerOverflowException if that doesn't fit in an int. The actual function contains more information that the spec, such as how exactly it checks for overflow and whether it calls a multiply instruction or does its own repeated addition and whether it does b multiplications or uses certain mathematical tricks to work faster. The proof on the other hand I think does have to be as complex as the function, but at least proofs tend to be written in ways that the computer can help prove them.

magic_haze 16y ago
Why so condescending? Joel made a perfectly valid point, and while _you_ might be thinking of something specific while writing your answer, many of us here don't have that context. I just spent the last few minutes trying to understand the last paragraph, and I'm still confused. I thought it was an accepted axiom that no "perfect" specs can be written in natural language: sure, you can _try_ to with a great deal of effort, but you can never get the same guarantees that a mathematically-based technique can give you. And the separation between the spec and the "proof" bothers me: what is the point of a spec if, after building a product, you can't verify you built it right? I would consider such specs as incomplete.
- tbrownaw 16y ago
  > And the separation between the spec and the "proof" bothers me: what is the point of a spec if, after building a product, you can't verify you built it right? I would consider such specs as incomplete. You have a spec, that says what the code should do. This is independent of the code; there can be many ways to write the code to match a given spec. You have a proof, that says what the code does do. This is intimately tied to the code, and with the right languages and tools can be the code. You verify that you built it right, by seeing that they match. This is abstraction, the basic interface/implementation distinction; the spec is an interface and the code+proof is an implementation.

magic_haze 16y ago

Why so condescending? Joel made a perfectly valid point, and while _you_ might be thinking of something specific while writing your answer, many of us here don't have that context. I just spent the last few minutes trying to understand the last paragraph, and I'm still confused. I thought it was an accepted axiom that no "perfect" specs can be written in natural language: sure, you can _try_ to with a great deal of effort, but you can never get the same guarantees that a mathematically-based technique can give you. And the separation between the spec and the "proof" bothers me: what is the point of a spec if, after building a product, you can't verify you built it right? I would consider such specs as incomplete.

tbrownaw 16y ago
> And the separation between the spec and the "proof" bothers me: what is the point of a spec if, after building a product, you can't verify you built it right? I would consider such specs as incomplete. You have a spec, that says what the code should do. This is independent of the code; there can be many ways to write the code to match a given spec. You have a proof, that says what the code does do. This is intimately tied to the code, and with the right languages and tools can be the code. You verify that you built it right, by seeing that they match. This is abstraction, the basic interface/implementation distinction; the spec is an interface and the code+proof is an implementation.