Verifying Specifications
So, the bottom line is that if there really were a mechanical way to prove things about the correctness of a program, all you’d be able to prove is whether that program is identical to some other program that must contain the same amount of entropy as the first program, otherwise some of the behaviors are going to be undefined, and thus unproven. So now the spec writing is just as hard as writing a program, and all you’ve done is moved one problem from over here to over there, and accomplished nothing whatsoever.
It’s true that you can’t make the programming, and thus the “entropy,” go away. But abstraction means that you can do more than just push the problem from one side to another. You can change its form. It’s like how some operations are easier in the frequency domain than in the time domain. The idea is that you write the specification in a high-level language, perhaps one that’s functional or declarative, that’s suited for reasoning about correctness. Then you have a compiler, which you trust, that converts it to executable code. This isn’t so useful if you’re unable to abstract your specification much from your program, but that’s hardly an indictment of specifications or formal verification. It just means that they aren’t applicable to every problem.
4 Comments RSS · Twitter
Brian Cantrill said the following in his Google Tech talk on DTrace (2007-8-15) that I think has some relevance here:
In software the blueprints are the machine. In software once you design the thing you've built it: the design is the machine. That's why the waterfall model is so fundamentally flawed. This idea that you could design the design before you design it, which is what the waterfall model is essentially saying, is flawed. Software is both, it's both information and machine.
http://video.google.com/videoplay?docid=-8002801113289007228
David: As Michael pointed out, what really matters here is the level of abstraction you use for your specification.
Specifications in natural language are not suitable to compile a program from but, if you omit a sufficient amount of detail, are comparatively easy to read and write.
Specifications in Java or C code are very detailed and hard to write, but can be compiled into an executable.
Maybe model-driven development is a step towards a suitable compromise: if you design a domain-specific metamodel for a range of programs you need to build, you can make sure it's reasonably easy to read and write for humans as well as easy for a machine to generate a program from. Of course the waterfall argument is still valid, since parts of specification, design and implementation merge into the modeling process.
David: I agree about the problems of the waterfall model. Still, I think that in many kinds of software there is some design, an algorithmic core or protocol, that’s separable from the implementation. This is the part that you might want a specification for.
Glad to see I'm not the only one having a funny feeling reading the talk. I like the Laplace analogy a lot!