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.

Meaning what? This needs to be explained better.