3 ms·
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'
by 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.