alt Hacker NewsSee also: https://juxt.github.io/allium/ (not affiliated in any way, just an interesting project)
I'm using something similar-ish that I build for myself (much smaller, less interesting, not yet published and with prettier syntax). Something like:
a->b # b must always be true if a is true
a<->b # works both ways
a=>b # when a happens, b must happen
a->fail, a=> fail # a can never be true / can never happen
a # a is always true
Product.alcoholic? Product in Order.lineItems -> Order.customer.can_buy_alcohol?
u1 = User(), u2=User(), u1 in u2.friends -> u2 in u1.friends
new Source() => new Subscription(user=Source.owner, source=Source)
Source.subscriptions.count>0 # delete otherwise
Allium looks interesting, making behavioral intent explicit in a structured format rather than prose is very close to what I'm trying to do with Ossature actually.
Ossature uses two markdown formats, SMD[1] for describing behavior and AMD for structure (components, file paths, data models). AMDs[2] link back to their parent SMD so behavior and structure stay connected. Both are meant to be written, reviewed, and/or owned by humans, the LLM only reads the relevant parts during generation. One thing I am thinking about for the future is making the template structure for this customizable per project, because "spec" means different things to different teams/projects. Right now the format is fixed, but I am thinking about a schema-based way to declare which sections are required, their order, and basic content constraints, so teams can adapt the spec structure to how they think about software without having to learn a grammar language to do it (though maybe peg-based underneath anyway, not sure).
The formal approach you describe is probably more precise for expressing system properties. Would be interesting to see how practical it is to maintain it as a project grows.
1: https://docs.ossature.dev/specs/smd.html
2: https://docs.ossature.dev/specs/amd.html