It sounds like you know what you’re doing but the documentation seems rather shallow and I don’t quite get it. I think you’re going to need a real language specification. I like how Go does it.
There is some apparently AI-generated prose that needs rewriting for clarity. For example, in the tutorial:
> The caller proves where; the implementation proves ensures. A precondition failure stops compilation before any program runs.
Fron the readme:
> I think you get it now.
Nope, I skimmed, because the syntax is unfamiliar.
> Memory model is in a tree of "planes". The stack is a tree. Each function is a node. Each variable is another node. If it's a struct then it's also a node. Down to the most atomic types, which are just the integers.
There is some apparently AI-generated prose that needs rewriting for clarity. For example, in the tutorial:
> The caller proves where; the implementation proves ensures. A precondition failure stops compilation before any program runs.
Fron the readme:
> I think you get it now.
Nope, I skimmed, because the syntax is unfamiliar.
> Memory model is in a tree of "planes". The stack is a tree. Each function is a node. Each variable is another node. If it's a struct then it's also a node. Down to the most atomic types, which are just the integers.
Meaning what? This needs to be explained better.