211–220 of 304 posts
THe HN title seems very misleading to me. How is this, in any sense of the word, "formal?" I don't see that particular word used to describe this tool on the web page itself. The site does describe it as a "programming language," which feels like a novel use of the term to me. The borders around a term like "programming language" are inherently fuzzy, but something like "code generation tool" better describes CodeSpe…
This is actually... pretty cool? Definitely won't use it for prod ofc but may try it out for a side-project. It seems that this is more or less: - instead of modules, write specs for your modules - on the first go it generates the code (which you review) - later, diffs in the spec are translated into diffs in the code (the code is *not* fully regenerated) this actually sounds pretty usable, esp. if someone likes writ…
We tend to obsess over abstractions, frameworks, and standards, which is a good thing. But we already have BDD and TDD, and now, with english as the new high-level programming language, it is easier than ever to build. Focusing on other critical problem spaces like context/memory is more useful at this point. If the whole purpose of this is token compression, I don't see myself using it.
LLMs works on both translation steps. But you end up with an healthy amount of tests.
I tagged each tests with the id of the spec so I do get spec to test coverage as well.
Beside standard code coverage given by the tests.
Its early for April fools
"Please don't post shallow dismissals, especially of other people's work. A good critical comment teaches us something."
I think this is 100% the right direction: Instead of imperatively letting the agents hammer your codebase into shape through a series of prompts, you declare your intent, observe the outcome and refine the spec. The agents then serve as a control plane, carrying out the intent.
What I found more useful is an extra step. Spec to tests, and then red tests to code and green tests. LLMs works on both translation steps. But you end up with an healthy amount of tests. I tagged each tests with the id of the spec so I do get spec to test coverage as well. Beside standard code coverage given by the tests.
For now, it's only about test coverage of the code, but the spec coverage is coming too.
What I found more useful is an extra step. Spec to tests, and then red tests to code and green tests. LLMs works on both translation steps. But you end up with an healthy amount of tests. I tagged each tests with the id of the spec so I do get spec to test coverage as well. Beside standard code coverage given by the tests.
This doesn't make too much sense to me. * This isn't a language, it's some tooling to map specs to code and re-generate * Models aren't deterministic - every time you would try to re-apply you'd likely get different output (without feeding the current code into the re-apply and let it just recommend changes) * Models are evolving rapidly, this months flavour of Codex/Sonnet/etc would very likely generate different co…
formal specification is no different from code: it will have bugs :)
There's no free lunch here: the informal-to-formal transition (be it words-to-code or words-to-formal-spec) comes through the non-deterministic models, period.
If we want to use the immense power of LLMs, we need to figure out a way to make this transition good enough
Earlier quoted context omitted.
Models aren't deterministic - every time you would try to re-apply you'd likely get different output (without feeding the current code into the re-apply and let it just recommend changes) If the result is always provably correct it doesn't matter whether or not it's different at the code level. People interested in systems like this believe that the outcome of what the code does is infinity more important than the co…
I would be very comfortable with - re-run 100 times with different seeds. If the outcome is the same every time, you're reliably good to go.