A sufficiently detailed spec is code
46 points by Gabriella439
46 points by Gabriella439
It's often easier to assert high-level properties of a system than implement them.
what do you mean by this? If by "assert" you mean verify, verification of anything is almost never done, let alone "easy." But I might be missing what you mean.
Checking if a number is prime is easier than generating a prime number. Checking vs constructing is asymmetrical for lots and lots of things.
Other examples:
But checking that an algorithm correctly generates prime numbers (as opposed to checking one specific output of that algorithm) is not necessarily easier than writing the algorithm
I wouldn't call that asserting a property though. You're talking about checking a single case, that's not a system-level property.
Asserting that a prime number generator always generates a prime number is likely more difficult than producing prime numbers.
In a design process, assertions compose trivially - just assert all of them. Sure, you might get an unsatisfiable set of assertions, but that's the only failure mode. Implementation details can be incompatible with each other in arbitrarily complex ways.
An example: the JavaScript specification is very detailed, to the point that there are multiple projects (ecmaspeak, esmeta) which attempt to derive a fully executable JavaScript interpreter from just the specification. And they kind of work! We've gone to a great deal of effort to make the spec clear and consistent, and indeed it strongly resembles code most of the time.
But. The specification leaves the hard parts of a production JS implementation completely unspecified. For example, it says nothing whatsoever about how to implement garbage collection. And while there is a detailed (and formally verified) memory model for SharedArrayBuffers, you are left completely on your own as to how to actually implement shared-memory multithreading in a manner consistent with the memory model. Even Maps and Sets are specified as a simple list of key-value pairs (but the spec requires you to have sub-linear performance for various operations, so you must use a different implementation).
In our case, I think it is correct to say that the specification is simpler than the corresponding code, at least when speaking of production engines like V8. But it is also true that you cannot get remotely close to deriving a production engine merely from the specification.
JS is not the best here. This works well enough for a formally specified language. Scheme, ADA, Standard ML have formal specs that define this much better than JS. The dynamic typing story in JS is hell for static analysis.
I don't think what you wrote is very relevant to the parent comment
Scheme and Standard ML likely share the same property mentioned -- their spec doesn't say anything about garbage collection.
That alone makes the implementation longer than the spec.
I don't think Scheme and Standard ML have threads either, so they don't have an analogue of the SharedArrayBuffer issue
I think you are conflating two issues: the language design of JavaScript, and the quality of the spec (and its length with compared with the length of an implementation)
Very thoughtful post, though I respectfully disagree with the main premise.
As far as measurable evidence of my disagreement, there is still a large gap between the spec here and the implementation. I ran cloc on the repo, and there's 3,388 lines of Markdown to 16,063 lines of Elixir. So it's not like the generated code is a 1:1 mapping of the Markdown spec.
As far as my philosophical position, which to be clear I'm biased in because I'm heavily in favor of specification:
Specifications are necessary, and are sorely missed in our industry. Djikstra himself was a proponent of specification. And I quote:
It is our position that a solid product consists of a triple: a program, a functional specification, and a proof that the program meets the functional specification.
So, there must be some separation of the code from its specification, else we can't ever make a statement about the code's correctness. We can debate what those specifications look like (how much or how little detail they should reference, whether or not they're Hoare-logic style or refinement style, etc.), but we can't just say "the code is the code, and that's it."
Now, it's a very valid question as to whether or not an AI prompt counts as a specification. I actually don't think it does! So maybe we're in agreement there. I'm more fond of executable specifications, e.g. as produced in a language like Quint. An LLM can help you create such specifications, but since they're used as tools for verification I think you should spend extra care validating the specs themselves, manually.
Prose specs are not specs… you can’t check what they specify. On the other hand a formal spec can nicely expand to hundreds of times the original code.
I've experienced this first hand. To validate the concept of a project I'm working on I developed a detailed spec of the behavior fleshed out with the help of AI. I used that spec as a guide to have an agent build a proof of concept for me. After having cleaned up the codebase from what it produced, the resulting code is actually shorter than the spec! And of course the process of actually implementing it exposed many areas of the spec that were ambiguous and needed correcting.
You simply cannot predict the final shape of a project up front. You need to experiment and get your hands dirty and try different approaches, and the only way to do that properly with enough fidelity to ensure you are actually building the right thing is to read and understand the code.
AI is incredibly effective at accelerating what you do. It helped me do research, it helped me spec it out and figure out a lot of edge cases ahead of time, it helped me prototype it, it helped me test it, it helped me iterate on it, and it helped me refactor it.
But I absolutely could not stop at the spec level and expect it to produce a result that was remotely adequate for the project.
Where I don't quite agree with the author is this:
Specifications were never meant to be time-saving devices. If you are optimizing for delivery time then you are likely better off authoring the code directly rather than going through an intermediate specification document.
Working with a spec was absolutely a time saving device, but not in terms of saving time producing the final result, but rather saving time by not wasting time building the wrong thing.
A specification is by definition an approximation, and very rarely do we have a fully fleshed out vision of what to build in our heads before we build it. By approximating a problem we can quickly iterate on it and simulate the complete project through a lower fidelity mockup. Simply working on the specification saved me time by exposing issues that I did not think of at a high level. Then, having AI produce a rough proof of concept helped surface which areas needed the most work, and which concepts did not work as elegantly as I had hoped ahead of time. AI was able to handle the easier parts well so I could focus my attention on the hardest parts.
More generally, the principle of "garbage in, garbage out" applies here. There is no world where you input a document lacking clarity and detail and get a coding agent to reliably fill in that missing clarity and detail. Coding agents are not mind readers and even if they were there isn't much they can do if your own thoughts are confused.
This is absolutely correct, however I think it's missing the bigger picture which is that sometimes the hardest part of a project is finding the garbage. Working with AI exposed the limits of my understanding of my own project much faster than if I were to do an earnest attempt by hand. Even where the AI made stupid assumptions, it still exposed areas of my specification and understanding that were not fully thought out. Agents are indeed not mind readers, but the practice of asking them to try has been the most effective way for me to recognize where my own thoughts are confused.
I think the overarching message is correct here. AI cannot build something for you when you don't know in minute detail what you want, but I think the continuation of that thought is that AI exposes where you don't know what you want and iterating with AI is very powerful for refining your ideas quickly.