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.

This language has been something I've wanted to build for years. For a while I thought I'd get my PhD and build it there. But now it's very possible to have Claude build it while I'm at work and give it intense code review every day. It's still not in a "useful" place yet, but I'm curious what fellow programmers think of a language like this. If I continue work is this something anyone thinks they'd enjoy using? Would love some feedback, thanks!

That's basically SPARK (the Ada subset) but with c-like syntax (more or less).

Sorry for the non constructive comment:

I wish we would stop xxx::yyy::zzz for namespace.

It was horrible in C++ from day one, and is still horrible in Rust.

It had some reason to be this way in C++ but not in any other newer language.

Real negative part: it looks to me that the authors of those languages are parroting other languages rather than understanding the reason of those language choice.

This simply worries me because I judge the level of expertise and makes me not consider the language in the first place.

(I know C++ and Rust are alive but they share their fair share of poor design choice)

Is this just "Rust with dependent types"? Not saying that as a criticism, I think this is genuinely useful.

I didn't delve too deeply, but I don't get it. How do you get provable runtime safety (in a dependent types sense) in a system which gives you direct control over memory, and without introducing the kind of overhead that would be inappropriate for a systems language?

Your "overflow, then inspect" example illustrates this incoherency. If overflow is allowed, and you try to fit 250 + 10 into a u8, so the value should be 4, which is less than 10, so it should fit your precondition, not violate it. And this is a simple example where 250+10 is known at compile-time - what happens when a user provides the number at run-time? Does the compiler attempt to provide the proof anyway? How?

I mean.... I have a lot of respect for Haskell and Idris and the goals they set out. But they're not systems languages.

[dead]