Indeed, both Verus and Dafny are very close to home here — thanks for the pointer. I did feel at times that I might be reinventing the wheel a bit.
I also thought about pushing more toward Lean and theorem proving instead of a lighter SMT-style direction, but programming and mathematics diverge quickly unless that abstraction boundary is handled carefully. To me, though, that mostly concerns the L1 -> L2 step.
L2 is still the least settled layer and the one I am actively exploring. The idea there is to let relations acquire semantic interpretations: this relation may be realized as a class, an embedding, a parser, etc. Since there is often more than one valid implementation route, I want that choice to be explicit.
And yes, part of the point is exactly to constrain and verify that the end result still matches the original intent at some IR/formal level.
So I am beginning to think the layering does offer something beyond plain Markdown specs. L1, at least as I currently see it, is intentionally very small: just types and relations, in a logic-oriented style somewhat closer to Prolog — or even SQL — where the world is modeled relationally and constraints are expressed over that. Essentially having more than one targets on L2 level (at the same time in one module) will help to generate both the code and the semantical verification. That's actually a very fruitful observation - big thanks!
`len` is an experiment in making specifications more central than code itself. The rough model is:
* write intent and examples in natural language
* capture the core structure with types, relations, and contracts
* describe how that model should map to concrete generated code
In the repo I currently call those layers L0, L1, and L2.
This is very much an early project. The current tooling is a small Go CLI that validates the structure of `.l1` files, and the language design is still evolving. So this is not a polished “look what I built” launch.
I’m sharing it because I’d like honest feedback on whether the core idea is interesting, confused, redundant with existing tools, or maybe useful in some narrower niche.
Comments, criticism, and pointers to similar work would be very welcome.
I also thought about pushing more toward Lean and theorem proving instead of a lighter SMT-style direction, but programming and mathematics diverge quickly unless that abstraction boundary is handled carefully. To me, though, that mostly concerns the L1 -> L2 step.
L2 is still the least settled layer and the one I am actively exploring. The idea there is to let relations acquire semantic interpretations: this relation may be realized as a class, an embedding, a parser, etc. Since there is often more than one valid implementation route, I want that choice to be explicit.
And yes, part of the point is exactly to constrain and verify that the end result still matches the original intent at some IR/formal level.
I have been experimenting with this in a calculator/parser example, where the pieces are starting to come together more nicely: https://github.com/ewiger/len/tree/main/examples/advanced/ca...
So I am beginning to think the layering does offer something beyond plain Markdown specs. L1, at least as I currently see it, is intentionally very small: just types and relations, in a logic-oriented style somewhat closer to Prolog — or even SQL — where the world is modeled relationally and constraints are expressed over that. Essentially having more than one targets on L2 level (at the same time in one module) will help to generate both the code and the semantical verification. That's actually a very fruitful observation - big thanks!