4 ms·

If we were able to write a complete, correct, and machine-readable specification for a piece of code, then we wouldn't need the code: we could use the specifica

If we were able to write a complete, correct, and machine-readable specification for a piece of code, then we wouldn't need the code: we could use the specification as the code. (This does not mean that programs cannot be verified; I believe they can be, at least to the same degree bulletproof vests are, and people routinely bet their life to demonstrate the latter. It's just that it shouldn't require two specifications.)

kazinator 5y ago
We would still need code because the "specification" and "code" have become synonymous by virtue of the specification becoming executable. It isn't possible to need the specification, but not need the code, when they are the same thing. The problem is that producing a complete and correct specification is almost of the same difficulty as producing complete and correct code. And the almost part disappears when we require the specification to be executable. Writers of non-executable specifications rely on being rescued by the code: that someone will "read between the lines" here and there when they produce the code. There is also a very good reason for needing two specifications: the specification proper and some code written to the specification (even if the specification is executable). Because producing specifications is difficult, the redundancy helps: whenever your specification and code have a discrepancy, that could be a defect. If specifications are executable, the implementations are severely constrained; they have to do exactly what the specification does. If the executable specification for a programming language is an interpreter for that language, then a compiled version of the language doesn't conform to the spec. It's a different spec.
- Mikhail_Edoshin 5y ago
  I'd argue that a specification must be a homomorphic version of the real code. A specification has fewer parts, but the relationships between the parts are same as in the code. I.e. it would be interesting to write a general specification for, say, a math typesetting algorithm and then add concrete specs that describe how that algorithm materializes in, say, different instruction sets. (I wish there were such specifications, because right now when you want to understand the general principle you have to rely on texts or dig that knowledge from the idiosyncrasies of different programming languages and individual styles.) I.e. a specification that can be shared between different programming environments. Something that captures the fundamental programming principles, not the "modern" features.
nayuki 5y ago
A specification isn't the same as executable code. For example, the specification for sorting any array A having indexes [0 .. n) is the resulting array B such that there exists a permutation P of [0 .. n) such that B[P(0)] <= B[P(1)] <= ... <= B[P(n-1)]. But this specification says nothing about how to find such a permutation. You could do it by brute force because the space is finite, but that wouldn't be a practical sorting algorithm. So a practical algorithm will have a different flavor and different proof than the simplest specification.
- Mikhail_Edoshin 5y ago
  It looks like too big a specification, more like a wish. We could equally well write that the result must be a solution to the traveling salesman problem. A specification can only be useful if there exist a piece of code that can take it, apply it to the algorithmic part and tell us the results. I'm thinking more along the lines of "when this field is X, that field can only be Y or Z" or "when this condition holds, these fields are not accessed". And these declarations should be a part of the main code so that it can refer to its internals.

kazinator 5y ago

We would still need code because the "specification" and "code" have become synonymous by virtue of the specification becoming executable. It isn't possible to need the specification, but not need the code, when they are the same thing. The problem is that producing a complete and correct specification is almost of the same difficulty as producing complete and correct code. And the almost part disappears when we require the specification to be executable. Writers of non-executable specifications rely on being rescued by the code: that someone will "read between the lines" here and there when they produce the code. There is also a very good reason for needing two specifications: the specification proper and some code written to the specification (even if the specification is executable). Because producing specifications is difficult, the redundancy helps: whenever your specification and code have a discrepancy, that could be a defect. If specifications are executable, the implementations are severely constrained; they have to do exactly what the specification does. If the executable specification for a programming language is an interpreter for that language, then a compiled version of the language doesn't conform to the spec. It's a different spec.

Mikhail_Edoshin 5y ago
I'd argue that a specification must be a homomorphic version of the real code. A specification has fewer parts, but the relationships between the parts are same as in the code. I.e. it would be interesting to write a general specification for, say, a math typesetting algorithm and then add concrete specs that describe how that algorithm materializes in, say, different instruction sets. (I wish there were such specifications, because right now when you want to understand the general principle you have to rely on texts or dig that knowledge from the idiosyncrasies of different programming languages and individual styles.) I.e. a specification that can be shared between different programming environments. Something that captures the fundamental programming principles, not the "modern" features.

nayuki 5y ago

A specification isn't the same as executable code. For example, the specification for sorting any array A having indexes [0 .. n) is the resulting array B such that there exists a permutation P of [0 .. n) such that B[P(0)] <= B[P(1)] <= ... <= B[P(n-1)]. But this specification says nothing about how to find such a permutation. You could do it by brute force because the space is finite, but that wouldn't be a practical sorting algorithm. So a practical algorithm will have a different flavor and different proof than the simplest specification.

Mikhail_Edoshin 5y ago
It looks like too big a specification, more like a wish. We could equally well write that the result must be a solution to the traveling salesman problem. A specification can only be useful if there exist a piece of code that can take it, apply it to the algorithmic part and tell us the results. I'm thinking more along the lines of "when this field is X, that field can only be Y or Z" or "when this condition holds, these fields are not accessed". And these declarations should be a part of the main code so that it can refer to its internals.