Does your tool attempt to mechanically create its own proof that the specification is satisfied by the code, or does that involve human effort? (Or both?)

That's pretty much it. The value is that tests can be automatically executed and verified. A specification document can't.

Writing a spec is still a step in the process - a bootstrapping step. The spec is a "write one to throw away" placeholder until you get far enough that the spec can be replaced with executable tests.

Take the IRC RFC, for instance. A lot of it is amenable to code generation, but machine-parsing the spec is so hard (I know.. I tried, many moons ago). I feel like a big chunk of that spec could be written in such way that a big part of an IRC client or server could be generated. For other parts, a generator could at least create boilerplate to be filled by a human and maybe some automatic tests.

The ones that fall in the middle are harmful.

It just leads to a million kind-of-similar things but because there's insufficient similarity you can't reap the benefits of having the spec (think automated documentation tools, pluggable APIs, client/server tools, etc).

It turns into a religion and a word that everyone ends up using but hardly any two people agree on exactly what it is.

If there's a spec for something it should have a corresponding verification tool that takes your stuff as input and basically validates it down to a yes/no answer. Your API is either compliant or not end of story. It shouldn't be a shade of grey that leaves room for arguments and lengthy blog posts about the philosophy of the spec.

The spec can still accommodate and allow for some uncertainty and flexibility but in a controlled manner and while maintaining an unambiguous specification.

Anyway, I regret the tone of my previous message, which mostly made me look foolish, and thank you for your kind response.

Canonically, within the industrial context, there are two processes for achieving compliance of implementation with specification ("correctness"). The first is testing, the second is formal verification. In either case, you need an artifact at a higher level of abstraction (the specification) and one at a lower level (the implementation).

In testing, someone who has access to the specification can evaluate the dynamic behavior of the implementation and determine whether it matches. In formal verification, you can do the same by static analysis and proof.

If you say "the code is the specification" then correctness becomes completely vacuous. The code is correct because it runs. Great. So what? If the implementation results in behavior that is completely unintended by the author (e.g. your smart contract contains a re-entrancy problem: a notorious source of bugs, or isn't robust to EVM stack exhaustion) and you still want to claim it's "correct" then I just don't know what to suggest - we're never going to agree, and I don't think your usage is anything like standard.

I could see potential in a function-level spec in the form of an append-only transcript, where only one line can be added at a time. So you (with your requirements-specifier hat on) write a line of spec; and then you (as the programmer) write a function that only does what the spec says, in the stupidest way possible; and then you put on the other hat and add another line to the spec to constrain yourself from doing things so stupidly; and on and on. The same sort of granularity as happens when doing TDD by creating unit tests that fail; but these "tests" don't need to execute, human eyes just need to check the function against them.

---

On another tangent: I've never seen anyone just "bite the bullet" on this, acknowledge that what they want is redundant effort, and explicitly design a programming language that forces you to program everything twice in two separate ways. It seems to me that it'd actually be a useful thing to have around, especially if it enforced two very different programming paradigms for the two formalisms—one functional and one procedural, say; or one dataflow-oriented ala APL or J, and the other actor-modelled ala Erlang.

Seems like something NASA would want to use for high-assurance systems, come to think of it. They get part-way there by making several teams write several isolated implementations of their high-assurance code—but it will likely end up having the same flaws in the same places, given that there's nothing forcing them to use separate abstractions.

There are many ways out there to write specifications. Some are good, some are bad. Let's assume we got a very good one. Then let's say I actually implement the specification correctly. So now I have a program and a spec it matches.

But then comes the problem: My application needs to change. Along with it, we need to change the specifications. If said specifications are too high level, then we start changing code without changing spec, and it doesn't take long before the spec is a dead document. If the spec is too low level, then change is hard, because the specification's friction becomes unbearable quickly.

So the problem quickly becomes the fact that writing specifications isn't really any easier than writing the code. It's the same problem that plagues many testing suites in practice: They either test too little, or test so much they increase the cost of development way past their value.

I am not saying we should not write tests, or specs. But what I really want to know is how to write a good spec, or a good test suite, because if those are bad quality, they actually become detrimental. At work, I just spent a solid two weeks trying to fix extremely overspecified tests: Hundreds of them that should have never been affected by the code changes. The people that write such tests will probably write terrible specifications that are just as brittle.

So don't show me a new specification language: Show me how said language makes it easy to write good specifications, and hard to write bad ones.

It's both a reasonable and unreasonable concept. It's unreasonable because it tries to turn programming into factory work, in fact you may even see them set up workflows predicated on an assembly line concept. This kind of works, and why it's kind of reasonable, when the work is sufficiently well-understood. It's very common in these systems to have a very detailed specification. Often the defects are deviations from the specifications that got through because of the manner in which these were classically tested (primarily integration tests, often manual, necessarily restricting the scope of the testing regimen). Other defects are realizations that the specification itself has an issue (happens), often the result of a dependence on a prose format for the specification which doesn't lend itself well to formal analysis. It also tends to, well, become wordy. 1000 page specs are not unheard of even for relatively small systems, you can imagine there may be quite a few pieces of conflicting information in there.

Specification "by example" is, in my experience, almost guaranteed to result in missed cases or unspecified behaviors in uncommon situations.

We'd mainly spend our time writing UML and thinking back to the bad old days when writing software was using old fashioned text editors like vim and emacs, and we'd be wondering how those fools managed to get anything done.

Meanwhile back in reality, it's the same old.

You simply DO THIS. It's not optional. It's not negotiable.

Also, calling this UX creeps me out :)

That said, maybe there's a need for something like that. A programmer could write an exceedingly thorough set of unit tests and let the synthesizer worry about how to satisfy those tests. Writing tests is almost universally simpler and easier than writing implementations. I can see the potential productivity enhancing value of that, especially in situations where I have to work in an unfamiliar framework. Like I might not know how to write an Electron app, but I could certainly write the unit tests to specify the front end behavior I want. A synthesizer could save me from having to learn all the nitty gritty framework specific techniques. Basically TDD without having to do the actual implementation. And eventually if the application required performance enhancements, a developer with the correct expertise could tune my synthesized code.

Because, right now, developing specifications is by far the hardest part of coding. But implementation is still not trivial in most cases. For certain use cases, it might be helpful to free up developer time to focus on specifications and QA instead of feature crunching.