Verifying Specifications

Joel Spolsky:

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.

Newton Storage History

Landon Dyer:

One afternoon Michael Culbert, the Newton technologist, came into my office to discuss battery contact bounce. I’d been nervous about the robustness of the storage system and had talked with him before about it, and now he confirmed my worst fears. Battery contact bounce is the jiggling of the power connectors when you toss a device onto a hard surface; the device can easily reset, and if the Newton was in the middle of a storage update, all the data would be lost. As I said, we’d been talking about doing transactions in the stores for a while, and Michael finally had a good argument for why they were going to be critical.