alt Hacker NewsAuthor here. The TL;DR: move rules from prompts into types the compiler refuses to violate, then bounce the AI coding loop off those refusals. The repo is github.com/pyrex41/Shen-Backpressure. Builds a lot on Geoff Huntley's backpressure idea -- none of this is rocket science, just an effort to apply sound programming principles in a world of LLM coding agents.
Replies
TBH something like this sounds useful even without LLMs (although I haven't fully grokked this yet). The problem with the operational level is that you can't express the invariants etc at the type level - not least because you're working across multiple languages - so the kind of dumb issues that we're beginning to rule out at the level of the language at the process level still require lots of diligence in operational code. Some kind of shared "operational type system" that could be integrated into relevant languages would potentially help a lot.
Thank you, interesting work. Please, clarify what is possibly a naive question - your README states that the constraints imposed by your tool are weaker than the formal verification guarantees. Why not implement the backpressure as the full formal verification barrier? Too complex to implement?
[dead]
This is great but keep in mind that Go allows the programmer skip these invariants in various ways.
I wish Go had a serious type system. Never mind algebraic types, but one that fucking respected private values and did things like validating enum values.