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.
I'd assume, what you do is based on some research, with articles and other projects like yours - these references are what's missing from your project, you don't have to write them yourself.
The most important missing explanation, that only you can provide, is this: Why a new language? There are projects that attach proof obligations to standard Rust in order to reuse its vast ecosystem and existing LLM skills. That would be a far easier and more productive approach to take.
Google has a two-part technical writing crash course:
- https://developers.google.com/tech-writing/one
- https://developers.google.com/tech-writing/two
Success in programming languages is not simply if-you-build-it-they-will-come. Bootstrapping a community that loves programming in it is the hard part. You'll either need a killer interop story with an already built ecosystem, or you'll need your own HTTP server, JSON parser, etc. etc. etc.
Best of luck! I'll watch this space.
That is good advice, I’m definitely planning on including some batteries soon, once I’m very happy with where the compiler is at.
Mine has a formally proven borrow checker built on linear types, along with algebraic effects, with an LLVM compiler written in lean -- the type checker uses exactly the proven calculus.
If you are going to build a language with claude, I highly, highly recommend writing it in Lean or Coq and starting by formalizing a pre-existing paper or system that has the properties you want.
Claude gets confused and takes shortcuts constantly, and if you don't have a proven base, you are really going ot struggle. I had to throw away months of work as i got bogged down trying to resolve special cases and bugs that just evaporated when i switched to a proven calculus.
That is exactly my motivation. The purpose of adding effects to my language, for example, was at least partially so you can track changes to things like IO usage in PRs. I also plan on adding a simple proof DSL that surfaces some lean functionality directly into the surface, so you can prove invariants about code as in this language, or surface exactly what is being trusted when writing the equivalent of unsafe code.
The main thing I am trying to solve is the LLM code review problem, really.
There are a shrinking number of reasons to geenfield projects with non-strict or unsafe languages now.
if you're all-in on ai, you want to prioritize familiarity for agents.
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)
I don't mean this to sound combative, but I think you are the one who doesn't understand the reason for the language choice. I assume you're objecting to the fact that these languages use different operators for module/namespace paths (`::`) and object member/method access (`.`), not the `::` symbol specifically.
You seem to assume that Rust blindly imitated C++, but that's not the case. The `::` syntax allows the compiler to identify and resolve all the static paths before any type inference or other analysis. This is important because macros are expanded between these stages, and can in turn introduce more static names which must also be resolved before any further compilation.
You might be able to introduce a rule that any `.`-path that can be resolved statically will be, trumping any non-static members (or maybe not, it might cause ambiguities I'm not thinking of), but Rust's stated design philosophy favors explicitness.
I don't know what this language's reason for using it was, as I don't see any mention of macros. But in general it simplifies compiler design. If you can resolve all the static names up front, the following compiler stages can ignore the concept of namespaces altogether.
However, I believe Rust purposely imitated C++, for reasons. And I still don't like it.
A lot of language are doing fine using dots. And if you are going to use '::' you can have your reasons. I would still find it annoying to type and read.
Just to add precision: I critic the syntax (which is very subjective), and I critic the parroting, as two separated arguments.
I have implemented one such language, and while it is indeed doing fine, the dots-everywhere syntax really does complicate name resolution. It only uses it because the distinction between two different operators would be lost on its intended less-technical audience. It is a (in my opinion unfortunate) tradeoff made for a specific reason.
And one thing those languages all (as far as I know) have in common is that they do not have Rust's macro system. It may well be impossible to implement that without a distinct operator.
I have no opinion as to whether that operator should be `::` or some other arbitrary symbol, but I believe that no matter what symbol they chose, someone would complain that it doesn't fit their personal taste. Can't please everybody.
I don't get it. Is it syntactically horrible or are there real reasons that I'm missing?
From "A History of C++: 1979− 1991".
> In C with Classes, a dot was used to express membership of a class as well as expressing selection of a member of a particular object. This had been the cause of some minor confusion and could also be used to construct ambiguous examples. To alleviate this, :: was introduced to mean membership of class and . was retained exclusively for membership of object.
It was taken from Algol68.
Then, this was reused for namespaces for consistency reason.
I write Rust mostly for my day job (and it's also my preferred language on the side these days), so I usually end up explicitly importing all the symbols I actually use because module::func is just additional noise in an already pretty verbose language and is what's considered 'idiomatic'.
I don't really get the issue with :: being the separator used here. It's slightly ugly, but it's visually distinct from . for field access, which I do appreciate.
I just like "dots" for everything, and there are some reasons to distinguish package/module qualification, struct/class member access (.), or static member access (::).
let x = vec![1,2,3]; let a = &mut x[0]; let b = &mut x[1]; swap(a, b);
This is not allowed. And actually in the compiler’s mind it’s for the same reason as this:
let x = vec![1,2]; let a = &mut x[0]; x.push(3); a = a + 1;
Which is definitely not safe and should be rejected. But the compiler cannot reason that the above case is actually safe, because they both fail to compile for lifetime reasons.
Another thing I’m working on are “patterns” which are like enums on steroids. In Rust you cannot define how an enum is laid out, thus requiring optimizations for types like Option<&T> to be in the compiler. In evergreen this will be in the language via a similar process to trait implementation.
How are you going to solve the problem with other means? Lifetimes basically guarantee, that there are no use-after-free bugs.
Each “where” is called a plane, which is a tree. The stack plane contains all your function calls memory, a structure allocated on the stack has a child plane for each field. The compiler tags which plane something is from at compile time and tracks when it dies.
Things do get complicated in scenarios like:
fn max(a: &usize, b: &usize) -> &usize {
if *a > *b { a } else { b }
In such a scenario the compiler tags the result with both of the input planes. However, you cannot define add a postcondition ensures clause to make it more precise
In a sibling comment I said the types seem more likely to be refinement (or Liquid) types instead of being full-spectrum dependent types. Is this correct? I certainly haven’t been through enough of the docs to be confident, but I took a swing when I posted my comment.
How are you doing resolution of your dependent(refined?) types? I've been using Z3, but you're clearly doing something else here.
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.
Your hardware does this OR You implement it in software