Spine: a language where parsing is a nondeterministic…
1 reactions
Spine: a language where parsing is a nondeterministic effect and the grammar grows as the program is read
I've been working on Spine for several years, and I think some of the ideas might be interesting to this community — especially the interaction between effects, verification, and parsing.
The short version: Spine is a language for modeling systems as structured descriptions — what exists, what can change, and what must always be true — that compiles to native code via Zig. The compiler is self-hosting (145 modules).
What I think is PL-interesting:
1. Parsing as a nondeterministic effect. Instead of a fixed grammar, Spine treats each parse step as an effect with preconditions and postconditions. A production rule consumes input tokens (linear resources), checks preconditions against the current parse state, and produces parsed structure as new facts. Those facts can enable new syntax — so the grammar grows as the program is read. Nondeterminism isn't managed away; it's a structured effect that the compiler reasons about.
This means domain-specific syntax isn't a macro system or a preprocessor. It falls out of the effect system: a domain module introduces new effects, and those effects expand the available grammar.
2. Effects with pre/postconditions, not just type signatures. Every state change in Spine declares what must be true before it can happen and what will be true afterward:
* TransferOwnership requires that the from\_agent owns the asset.
* TransferOwnership requires that the from\_agent has capability CanTransfer.
* TransferOwnership ensures that the to\_agent owns the asset.
* TransferOwnership ensures that the from\_agent no longer owns the asset.
This isn't just documentation — the compiler dispatches constraints to Z3 and generates TLA+/mCRL2 artifacts for temporal verification.
3. Bidirectional compilation via FLP correspondence. The compiler uses correspondence relations between Spine and Zig (inspired by the Functional-Logic Programming duality). Every compilation step has a reverse direction, so the compiler can check its own output. The self-hosting compiler compiles all its modules through this pipeline.
4. HoTT-inspired types with QTT resource tracking. Types can express "a list of exactly n elements" or "an asset with at most one owner." Linear resources (à la QTT) track ownership — including input tokens during parsing, which prevents the parser from accidentally consuming the same input twice.
What the surface syntax looks like (from a governed asset transfer system):
Alice owns Car.
Engine is part of Car.
it is obligatory that each Asset has at most 1 owner.
it is forbidden that an Agent transfers an Asset it does not own.
TransferRequested leads to TransferApproved.
TransferApproved leads to TransferCompleted.
within jurisdiction NL, it is obligatory that asset transfers above 10000 EUR require notarial approval \BW Art. 3:89\].
verify constraint SingleOwner via z3.
verify temporal AssetTransferProtocol via tla+.
Status: The compiler pipeline works and is self-hosting. It's not packaged for general use yet — I'm posting because I think the design ideas are worth discussing, not because there's a download link.
Links:
Site: [ https://spine-lang.org https://spine-lang.org
16-part article series walking through the design: https://spine-lang.org/articles/
Article on parsing as a nondeterministic effect: https://spine-lang.org/articles/16-future-directions-parsing-as-a-nondeterministic-effect.html
Discord: https://discord.gg/wAAx6GMj
Questions I'd genuinely like input on:
Are there other languages treating parsing as an effect? I know about parser combinators with monadic effects, but the "grammar grows from postconditions" angle seems underexplored.
The CNL (controlled natural language) surface syntax reads well but is divisive. Curious what this community thinks about readability vs. familiarity tradeoffs
#technology
I've been working on Spine for several years, and I think some of the ideas might be interesting to this community — especially the interaction between effects, verification, and parsing.
The short version: Spine is a language for modeling systems as structured descriptions — what exists, what can change, and what must always be true — that compiles to native code via Zig. The compiler is self-hosting (145 modules).
What I think is PL-interesting:
1. Parsing as a nondeterministic effect. Instead of a fixed grammar, Spine treats each parse step as an effect with preconditions and postconditions. A production rule consumes input tokens (linear resources), checks preconditions against the current parse state, and produces parsed structure as new facts. Those facts can enable new syntax — so the grammar grows as the program is read. Nondeterminism isn't managed away; it's a structured effect that the compiler reasons about.
This means domain-specific syntax isn't a macro system or a preprocessor. It falls out of the effect system: a domain module introduces new effects, and those effects expand the available grammar.
2. Effects with pre/postconditions, not just type signatures. Every state change in Spine declares what must be true before it can happen and what will be true afterward:
* TransferOwnership requires that the from\_agent owns the asset.
* TransferOwnership requires that the from\_agent has capability CanTransfer.
* TransferOwnership ensures that the to\_agent owns the asset.
* TransferOwnership ensures that the from\_agent no longer owns the asset.
This isn't just documentation — the compiler dispatches constraints to Z3 and generates TLA+/mCRL2 artifacts for temporal verification.
3. Bidirectional compilation via FLP correspondence. The compiler uses correspondence relations between Spine and Zig (inspired by the Functional-Logic Programming duality). Every compilation step has a reverse direction, so the compiler can check its own output. The self-hosting compiler compiles all its modules through this pipeline.
4. HoTT-inspired types with QTT resource tracking. Types can express "a list of exactly n elements" or "an asset with at most one owner." Linear resources (à la QTT) track ownership — including input tokens during parsing, which prevents the parser from accidentally consuming the same input twice.
What the surface syntax looks like (from a governed asset transfer system):
Alice owns Car.
Engine is part of Car.
it is obligatory that each Asset has at most 1 owner.
it is forbidden that an Agent transfers an Asset it does not own.
TransferRequested leads to TransferApproved.
TransferApproved leads to TransferCompleted.
within jurisdiction NL, it is obligatory that asset transfers above 10000 EUR require notarial approval \BW Art. 3:89\].
verify constraint SingleOwner via z3.
verify temporal AssetTransferProtocol via tla+.
Status: The compiler pipeline works and is self-hosting. It's not packaged for general use yet — I'm posting because I think the design ideas are worth discussing, not because there's a download link.
Links:
Site: [ https://spine-lang.org https://spine-lang.org
16-part article series walking through the design: https://spine-lang.org/articles/
Article on parsing as a nondeterministic effect: https://spine-lang.org/articles/16-future-directions-parsing-as-a-nondeterministic-effect.html
Discord: https://discord.gg/wAAx6GMj
Questions I'd genuinely like input on:
Are there other languages treating parsing as an effect? I know about parser combinators with monadic effects, but the "grammar grows from postconditions" angle seems underexplored.
The CNL (controlled natural language) surface syntax reads well but is divisive. Curious what this community thinks about readability vs. familiarity tradeoffs
#technology
1
| 4,000 mlx | |
| 6 | |
| 1 |