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.
Yeah the repo/documentation is pretty rough right now. TBH I am not quite ready to spend a ton of time on docs yet as some of these things are changing on the fly. But the core concept/syntax should remain the same. The code is not super interesting yet, though
> TBH I am not quite ready to spend a ton of time on docs yet as some of these things are changing on the fly.
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.
For me part of the fun of such a side project is complete control. I’m willing to risk this over starting from something existing, which may be the wrong call!
If you want to have an LLM write your README (and other docs), I've found it useful to add a DOCS-GUIDE.md to your project and write your conventions and expectations there.
Google has a two-part technical writing crash course:
I've had good success with adding a directive to the guide that points to those two URLs and tells the agent to adhere to them in all of its documentation.
I considered waiting longer to share more but felt feedback early was better than waiting for more polish. Will focus on this with high priority though, good feedback
I think you might want to more deeply consider the impact it has on people when you ask them to read a bunch of LLM-generated code and documentation that you haven't even taken the time to "polish" yet. Some (myself included) might consider it a violation of an implicit social contract to expect such disproportionate effort from your audience than you are willing to spend yourself upfront.
Maybe, to put it another way: Why should people want to spend time developing feedback for you when you were not willing to spend commensurate time on the things you want to show them first? You're putting the cart before the horse.
I agree with you, if I were asking for a code review. I'm mostly interested in what people think of the language features. A code review in its current state is not interesting, but I believe the site has some ideas that can be food-for-thought
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!
It's a really great concept. What guarantees are made by the prover?
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.
Thanks! The guarantee is that, without the use of trustme (which can prove any fact), you cannot address memory as the wrong type. The compiler also ensures that a pointer/reference to a value is live at compile time, so it’s not possible to create an invalid pointer (without the use of trustme). You can also claim any fact which the compiler must prove in order to continue compilation.
That is good advice, I’m definitely planning on including some batteries soon, once I’m very happy with where the compiler is at.
This isn't so much directed at you, as other people that get inspired by this. I have been working on my own Rust like language with claude for a few months and there are a _lot_ of projects like that out there.
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.
Is your language available anywhere? I'd be curious to check it out. I strongly believe that there will eventually be a new language created with agents in mind as the primary consumers, and making the foundations provable / safe are key cornerstones in my mind. The other property that I think is very important is fast tooling / compilation. Compilation speed is not generally the bottleneck right now in agent loops, but models can get faster, and as software scales up and is written by swarms of agents in concert, making the tools run really fast will be an important way to decrease cycle time and increase speed.
> I strongly believe that there will eventually be a new language created with agents in mind as the primary consumers
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.
This is cool! Thanks for sharing. I've been wanting something like this for a while
1. I'm curious how this handles I/O? Proving stuff is often really useful for distributed systems where we would like to prove our system behaves correctly under any ordering of I/O operations.
2. How does this compare to just using Rust and some proof tool like Kani or Verus?
Why optimize for old fashioned manual programming, especially since you are vibe coding the language to begin with? Unless you think Claude and friends will “enjoy” using it more.
To me it’s about determinism and feedback. Agents will make mistakes but if they get clear feedback from the tools they use, they will produce a good result.
There are a shrinking number of reasons to geenfield projects with non-strict or unsafe languages now.
The objective of this project isn't to make a language fit for AI to write but to make a "probably safe system language" regardless of who's doing the coding.
That would imply the AI should write every program in Python from now until the end of time; but just because the AI is most familiar with Python doesn’t mean we have to throw everything we know about system design and using the right tools for the job out of the window.
Not in every situation for all time, that's my point. Which language the AI should use will evolve over time as use cases and computing hardware evolve. It isn't the case that language design is now ossified at whatever existed in 2023.
Also, what you're saying implies Python and Rust should stop evolving as languages, as changing the language would invalidate the vast quantity of work the AI has been trained on.
> Not in every situation for all time, that's my point.
I disagree. It's not worth changing languages for new ones if you want to use AI, unless you can manage to create so much training data that it ends up baked into the models.
> Also, what you're saying implies Python and Rust should stop evolving as languages
Yes, much the way x86 assembly has stopped evolving for the user, outside of smallish additions like wider vector ops. Adding small, high value extensions extensions can be worth paying the token cost and increased failure rates if they add strong new capabilities.
If it's just ergonomic, it's a mistake, unless you want to target hand coders.
Just remember models are constantly evolving and being updated, so a language like python shouldn't stop evolving, models should keep updating themselves, for new languages too, it's only a matter of them getting traction and popularity, training data can be synthesized a posteriory using frontier models with extremely large contexts so you can always have the language spec and function reference.
I see minor differences; however, the author does nothing to highlight them. That's the number one thing that any new language should show when it's trying to fit into a niche that a language already exists for: What makes this language different?
I took a skim and I like the ideas, but you should go further with proving elements of real systems. For example, drivers for Linux, if your whole goal is to prove these things while being a systems language. Although I confess that I don't understand its output, are you using a compiler backend like LLVM? Should be in README.
Dependent types are part of it, yeah! There are definitely some things I dislike about Rust which I am not planning on including, mainly lifetimes and some ways they handle pointer mutability. One thing I particularly dislike about Rust is:
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.
The compiler statically tracks “where” everything lives. It also knows “when” the “where” is valid.
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
Sounds a lot like group borrowing from Valen, but that one still has annotations like `entity in world.entities[] mut`. Are you tracking the same things implicitly with post conditions?
Allocations live in their own plane, the root allocated typed being the root node of that plane. For threads, I’m still working on that, don’t have a super cool answer yet
Another thing - when a value is moved or dropped the plane’s type changes from T to shape(T). shape(T) contains unspecified data but has the size and alignment of a T. So you couldn’t safely prove that a moved out/dropped shape(T) is a T
This only works if you make every allocation its own plane, and scope all borrows to the lifetime of the plane, with a move terminating all borrows, at which point this is equivalent to rust, just with confusing jargon.
Correct, every allocation is its own plane. The nice thing about this model is that you don't need to explicitly call out lifetimes. I also believe that lifetimes aren't really a good model of what actually happens in memory. This model is more powerful because it understands relationships between planes in memory, which Rust's model doesn't. This is why it requires mutable borrows to be unique which is oftentimes overly restrictive. For instance this is not valid Rust:
let x = vec![1, 2, 3];
let a = &mut x[0];
let b = &mut x[1];
swap(a, b);
Because Rust doesn't really know the difference between the whole Vec an element within the vec. Therefore it treats any mutation as one that could potentially invalidate anything with the same lifetime and doesn't compile. So I believe the plane model to be strictly better because it allows for this and still prevents the real scary thing:
let x = vec![1, 2];
let a = &mut x[0];
x.push(3);
a = a + 1;
I’m not quite sure I understand your question. But if x is a vector of things that contain allocations, the compiler will track a plane for them and represent them sparsely as needed be.
The compiler tracks all of the currently living planes. The compiler tracks from which plane each borrow is borrowed. Once the plane it is borrowed from dies that borrow is no longer valid
Since you are replying, I’ll go ahead and you answer…
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.
What I’ve showcased is definitely not full fledged dependent types. Support is planned via ideal generics but it’s lower on the priority list to nail down
The introductory examples look more like refinement type (or Liquid types) which are limited to those operations and restrictions one’s that are provable by the compiler utilizing a restricted subset of operations and computational constructs subject to deterministic proving via SAT solving. I’m going to look closer at the docs so I could be mistaken on that point. It certainly seems to have taken the ownership and ‘borrowing’ concepts for memory semantics from Rust at a quick glance at the first few pages.
Dependent types can be achieved via “ideal Generics”. Very undocumented and not ready to commit to how they work yet, but the basic idea is that a type can be generic on a value.
Yeah it definitely looks like refinement vs actual dependent types. I do the same thing here[1] in my language (pardon the mess). Adding liquid types to basically rust is IMHO a good idea.
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)
> it looks to me that the authors of those languages are parroting other languages rather than understanding the reason of those language 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 have implemented one such language, and while it is indeed doing fine, the dots-everywhere syntax really does complicate name resolution.
Can you share an example? In my experience, this only happens with serious reuse of names across both types and values, e.g. with something like
struct a {
struct x {
typedef int y;
y x;
};
struct y {
typedef double x;
x y;
};
static x y;
y x;
};
a a;
after which the unified syntax "a.x.y" could either mean a typedefed int from struct x, or a double field from struct y... but why would you even want to support such scenarios? C++, for example, prohibits namespaces from sharing the names with types and values in the same scope, and even though it uses "::" for namespace lookups, it still had to introduce "typename" keyword to explicitly disambiguate the type names from values anyhow so...
For me, I guess it’s just that foo/bar is standard and fewer characters so it’s the obvious and ergonomic choice. But we can’t use that because of infix math, which is also a choice. So why are the choices made that way? “We made it easier to write mathematical notation at the expense of making it worse to talk about every namespace” isn’t the best trade off all the time.
I don't have a link but you can search on the web. I have the .pdf on my computer.
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.
My favorite namespacing syntax is ironically Clojures. module/func or fully.qualified.module/func or just func if you explicitly import the symbol. I vastly prefer shallow namespacing (module/func) most of the time.
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.
Don't think too much about it though, it was to express a personal opinion.
I just like "dots" for everything, and there are some reasons to distinguish package/module qualification, struct/class member access (.), or static member access (::).
Broadly speaking, does Evergreen allow me to prove/enforce more invariants than what Verus/rust allows? Evergreen certainly looks cleaner since its built in rather than bolted on.
AI has really lowered the bar to allow people to create new languages from scratch. I'm not repulsed by AI generated output as others are, so my critique does not fall along those lines. Actually, I think that more people can do this now means the bar has risen for what we should expect from these languages and their authors. Before a spec and a prototype implementation, and a willingness to learn was enough, but today I don't think that's the baseline, not anymore.
I understand the author has posted this, and explicitly several times in the README and here on HN has said this is a sketch and is for learning purposes and experimentation. That's great and I support such efforts wholeheartedly. So my criticism is given in the spirit that this project can be significantly improved.
However, the LLM presentation means the author has cosigned statements I don't think they should be cosigning.
For example, your homepage makes some pretty outrageous claims: for a language that didn't exist before last week, you're claiming it is "more powerful than C" and "safer than Rust". There is very little here to support these claims, and I think they should be retracted.
First, how is this language more powerful than C and why can't C adopt what this language does? Why can't C use your technique as a framework / preprocessor and do exactly what Evergreen does? If it's technically possible for C to do all this I don't think you can claim Evergreen is more powerful.
Also, I don't see any benchmarks, maybe I missed them. How can you claim the proofs don't affect performance? You say that the proofs are erased after they're checked but that doesn't necessarily mean there's no performance cost for having to write the code a particular way. To credibly make this claim you'll have to show proof.
And please when you do the benchmarks, make sure the AI actually optimizes the baseline version. There was another AI-authored language posted here recently which also made similar grand performance claims, but they didn't make sure they were being fair in what they were comparing: https://news.ycombinator.com/item?id=50238979. The AI will show your language is faster than Rust or C or whatever by writing suboptimal Rust / C.
When you say it's safer than Rust, you're leaving out that your system is incomplete and can't handle some things that Rust already handles, like sync + send. Moreover, the claim seems to be the existence of the features in your language defacto make it safer than Rust, but again that's not proven. Do they really? Also, several times in the Readme you claim Rust can't do particular things, when it actually can, just not statically e.g. using Rc and Refcell. In another case I don't think you're aware of https://doc.rust-lang.org/std/num/type.NonZeroU64.html.
Is the claim you can do those things where Rust can't, or that you can do them statically where Rust can only do it dynamically?
Finally, for some of these examples they seem to take a very long time to check, despite being so small. The overflow example takes almost 10 seconds on my machine, it's only 9 lines of code. How does this scale to an entire program? What's the largest program you've written to test this?
Anyway, I'm not saying any of this to discourage you, just to say that you really can't make the claims you're making without proof, and it's not enough to say "well the AI made the website and it's prone to making overblown claims without proof" -- no, when you publish them, the AI's words are your words. You can stand by what you can prove but otherwise you should be careful making grand claims.
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.
So it's Rust with compile-time checks? So its just Rust? What can be done in this language that can't be done in Rust with a macro?
```
macro_rules! nonzero {
($n:expr) => {{
const {
assert!($n != 0, "Non Zero Condition could not be verified");
}
$n as i64
}};
}
fn main() {
let x: i64 = nonzero!(0); // Throws verification error
};
```
If you need something to be provably mathematically correct you should write it in Lean, or Coq, some kind of dedicated verification program, if you merely need to guarantee certain conditions at runtime, you can just write some macros! I understand that they want certain facilities like proof by induction, and the ability to prove arbitrary theorems but why would you do that when you can write it in a dedicated language (Lean/Coq) that has been around for a long time, with far more tooling?
That aside, I think Evergreen is still a nice language, and can have applications, its just the ecosystem around it that needs development.
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.
Yeah the repo/documentation is pretty rough right now. TBH I am not quite ready to spend a ton of time on docs yet as some of these things are changing on the fly. But the core concept/syntax should remain the same. The code is not super interesting yet, though
> TBH I am not quite ready to spend a ton of time on docs yet as some of these things are changing on the fly.
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.
For me part of the fun of such a side project is complete control. I’m willing to risk this over starting from something existing, which may be the wrong call!
congrats & just fyi, you should put a "Show HN" if you are posting and presenting your own handiwork. Better optics.
Yeah, if I were motivated I’m sure I could figure it out from the tutorial.
And, to be clear, the README was mostly an initial prompt for the AI. I’ll prioritize making a much clearer and legible README soon
If you want to have an LLM write your README (and other docs), I've found it useful to add a DOCS-GUIDE.md to your project and write your conventions and expectations there.
Google has a two-part technical writing crash course:
I've had good success with adding a directive to the guide that points to those two URLs and tells the agent to adhere to them in all of its documentation.A good tip is to actually polish your README before sharing it with everyone.
I considered waiting longer to share more but felt feedback early was better than waiting for more polish. Will focus on this with high priority though, good feedback
I think you might want to more deeply consider the impact it has on people when you ask them to read a bunch of LLM-generated code and documentation that you haven't even taken the time to "polish" yet. Some (myself included) might consider it a violation of an implicit social contract to expect such disproportionate effort from your audience than you are willing to spend yourself upfront.
Maybe, to put it another way: Why should people want to spend time developing feedback for you when you were not willing to spend commensurate time on the things you want to show them first? You're putting the cart before the horse.
I agree with you, if I were asking for a code review. I'm mostly interested in what people think of the language features. A code review in its current state is not interesting, but I believe the site has some ideas that can be food-for-thought
Just want to say that you did a great job giving critique. Felt encouraging even though it's not even my project
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!
It's a really great concept. What guarantees are made by the prover?
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.
Thanks! The guarantee is that, without the use of trustme (which can prove any fact), you cannot address memory as the wrong type. The compiler also ensures that a pointer/reference to a value is live at compile time, so it’s not possible to create an invalid pointer (without the use of trustme). You can also claim any fact which the compiler must prove in order to continue compilation.
That is good advice, I’m definitely planning on including some batteries soon, once I’m very happy with where the compiler is at.
> You'll either need a killer interop story with an already built ecosystem
On that note: allow me to "import" or "use" a C header without writing any FFI code.
This isn't so much directed at you, as other people that get inspired by this. I have been working on my own Rust like language with claude for a few months and there are a _lot_ of projects like that out there.
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.
Is your language available anywhere? I'd be curious to check it out. I strongly believe that there will eventually be a new language created with agents in mind as the primary consumers, and making the foundations provable / safe are key cornerstones in my mind. The other property that I think is very important is fast tooling / compilation. Compilation speed is not generally the bottleneck right now in agent loops, but models can get faster, and as software scales up and is written by swarms of agents in concert, making the tools run really fast will be an important way to decrease cycle time and increase speed.
I was thinking about this problem and found a while ago that Unison lang has a cool concept, I recommend you give it a read [0].
- [0] https://www.unison-lang.org/docs/the-big-idea/
> I strongly believe that there will eventually be a new language created with agents in mind as the primary consumers
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.
This is cool! Thanks for sharing. I've been wanting something like this for a while
1. I'm curious how this handles I/O? Proving stuff is often really useful for distributed systems where we would like to prove our system behaves correctly under any ordering of I/O operations.
2. How does this compare to just using Rust and some proof tool like Kani or Verus?
Why optimize for old fashioned manual programming, especially since you are vibe coding the language to begin with? Unless you think Claude and friends will “enjoy” using it more.
Because good tools are good
It's so strange how much effort goes into producing a language that people don't even intend to write.
To me it’s about determinism and feedback. Agents will make mistakes but if they get clear feedback from the tools they use, they will produce a good result.
There are a shrinking number of reasons to geenfield projects with non-strict or unsafe languages now.
What's strange is only seeing value in manually writing code when clearly AI is very useful to produce quality code here.
you can ask ai to write code in existing languages with large training sets, and it'll do better because of the large volume of training data.
if you're all-in on ai, you want to prioritize familiarity for agents.
The objective of this project isn't to make a language fit for AI to write but to make a "probably safe system language" regardless of who's doing the coding.
That would imply the AI should write every program in Python from now until the end of time; but just because the AI is most familiar with Python doesn’t mean we have to throw everything we know about system design and using the right tools for the job out of the window.
Yes, Python or Rust would make sense to use as long as you're planning on sticking with LLMs.
Not in every situation for all time, that's my point. Which language the AI should use will evolve over time as use cases and computing hardware evolve. It isn't the case that language design is now ossified at whatever existed in 2023.
Also, what you're saying implies Python and Rust should stop evolving as languages, as changing the language would invalidate the vast quantity of work the AI has been trained on.
> Not in every situation for all time, that's my point.
I disagree. It's not worth changing languages for new ones if you want to use AI, unless you can manage to create so much training data that it ends up baked into the models.
> Also, what you're saying implies Python and Rust should stop evolving as languages
Yes, much the way x86 assembly has stopped evolving for the user, outside of smallish additions like wider vector ops. Adding small, high value extensions extensions can be worth paying the token cost and increased failure rates if they add strong new capabilities.
If it's just ergonomic, it's a mistake, unless you want to target hand coders.
Just remember models are constantly evolving and being updated, so a language like python shouldn't stop evolving, models should keep updating themselves, for new languages too, it's only a matter of them getting traction and popularity, training data can be synthesized a posteriory using frontier models with extremely large contexts so you can always have the language spec and function reference.
That's basically SPARK (the Ada subset) but with c-like syntax (more or less).
I see minor differences; however, the author does nothing to highlight them. That's the number one thing that any new language should show when it's trying to fit into a niche that a language already exists for: What makes this language different?
A compare and contrast is good feedback, will work on this
I took a skim and I like the ideas, but you should go further with proving elements of real systems. For example, drivers for Linux, if your whole goal is to prove these things while being a systems language. Although I confess that I don't understand its output, are you using a compiler backend like LLVM? Should be in README.
Is this just "Rust with dependent types"? Not saying that as a criticism, I think this is genuinely useful.
Dependent types are part of it, yeah! There are definitely some things I dislike about Rust which I am not planning on including, mainly lifetimes and some ways they handle pointer mutability. One thing I particularly dislike about Rust is:
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.
> not planning on including, mainly lifetimes and some ways they handle pointer mutability
How are you going to solve the problem with other means? Lifetimes basically guarantee, that there are no use-after-free bugs.
The compiler statically tracks “where” everything lives. It also knows “when” the “where” is valid.
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 {
}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
Sounds a lot like group borrowing from Valen, but that one still has annotations like `entity in world.entities[] mut`. Are you tracking the same things implicitly with post conditions?
And what about allocations and threads?
Allocations live in their own plane, the root allocated typed being the root node of that plane. For threads, I’m still working on that, don’t have a super cool answer yet
how does that prevent use after free? pretty sure your algorithm is either very poorly explained or doesnt' actually work.
Another thing - when a value is moved or dropped the plane’s type changes from T to shape(T). shape(T) contains unspecified data but has the size and alignment of a T. So you couldn’t safely prove that a moved out/dropped shape(T) is a T
This only works if you make every allocation its own plane, and scope all borrows to the lifetime of the plane, with a move terminating all borrows, at which point this is equivalent to rust, just with confusing jargon.
Correct, every allocation is its own plane. The nice thing about this model is that you don't need to explicitly call out lifetimes. I also believe that lifetimes aren't really a good model of what actually happens in memory. This model is more powerful because it understands relationships between planes in memory, which Rust's model doesn't. This is why it requires mutable borrows to be unique which is oftentimes overly restrictive. For instance this is not valid Rust:
let x = vec![1, 2, 3]; let a = &mut x[0]; let b = &mut x[1]; swap(a, b);
Because Rust doesn't really know the difference between the whole Vec an element within the vec. Therefore it treats any mutation as one that could potentially invalidate anything with the same lifetime and doesn't compile. So I believe the plane model to be strictly better because it allows for this and still prevents the real scary thing:
let x = vec![1, 2]; let a = &mut x[0]; x.push(3); a = a + 1;
How about `x[i] = 7`? What if x is a vector of values that contain allocations?
I’m not quite sure I understand your question. But if x is a vector of things that contain allocations, the compiler will track a plane for them and represent them sparsely as needed be.
The compiler tracks all of the currently living planes. The compiler tracks from which plane each borrow is borrowed. Once the plane it is borrowed from dies that borrow is no longer valid
If you can replace elements in a vector you can make elements unreachable.
Since you are replying, I’ll go ahead and you answer…
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.
What I’ve showcased is definitely not full fledged dependent types. Support is planned via ideal generics but it’s lower on the priority list to nail down
The introductory examples look more like refinement type (or Liquid types) which are limited to those operations and restrictions one’s that are provable by the compiler utilizing a restricted subset of operations and computational constructs subject to deterministic proving via SAT solving. I’m going to look closer at the docs so I could be mistaken on that point. It certainly seems to have taken the ownership and ‘borrowing’ concepts for memory semantics from Rust at a quick glance at the first few pages.
Dependent types can be achieved via “ideal Generics”. Very undocumented and not ready to commit to how they work yet, but the basic idea is that a type can be generic on a value.
How long have you been working on this?
I have been building little prototype languages for years. This iteration which is heavily AI powered is a couple weeks old
Oh cool, it's amazing how quickly you can stand up a language now, I love it. I'd love to exchange ideas, I really like what you're doing.
How are you doing resolution of your dependent(refined?) types? I've been using Z3, but you're clearly doing something else here.
Yeah it definitely looks like refinement vs actual dependent types. I do the same thing here[1] in my language (pardon the mess). Adding liquid types to basically rust is IMHO a good idea.
[1] https://march-lang.org/docs/refinement-types/
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)
> it looks to me that the authors of those languages are parroting other languages rather than understanding the reason of those language 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.
I assumed Evergreen blindly imitated Rust.
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.
> A lot of language are doing fine using dots.
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 have implemented one such language, and while it is indeed doing fine, the dots-everywhere syntax really does complicate name resolution.
Can you share an example? In my experience, this only happens with serious reuse of names across both types and values, e.g. with something like
after which the unified syntax "a.x.y" could either mean a typedefed int from struct x, or a double field from struct y... but why would you even want to support such scenarios? C++, for example, prohibits namespaces from sharing the names with types and values in the same scope, and even though it uses "::" for namespace lookups, it still had to introduce "typename" keyword to explicitly disambiguate the type names from values anyhow so...> It was horrible in C++ from day one, and is still horrible in Rust.
I don't get it. Is it syntactically horrible or are there real reasons that I'm missing?
For me, I guess it’s just that foo/bar is standard and fewer characters so it’s the obvious and ergonomic choice. But we can’t use that because of infix math, which is also a choice. So why are the choices made that way? “We made it easier to write mathematical notation at the expense of making it worse to talk about every namespace” isn’t the best trade off all the time.
No it's just a personal opinion. I like the UX of using dots for everything.
Any links to the historical reason for C++ using ::?
I don't have a link but you can search on the web. I have the .pdf on my computer.
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.
My favorite namespacing syntax is ironically Clojures. module/func or fully.qualified.module/func or just func if you explicitly import the symbol. I vastly prefer shallow namespacing (module/func) most of the time.
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.
Hard agree. PHP did it right with backslashes.
That, sir, is a hot take
I'm assuming it was a joke. I'm hoping it was a joke. Please assure me it was a joke.
This is good feedback. I will chew on this…
Don't think too much about it though, it was to express a personal opinion.
I just like "dots" for everything, and there are some reasons to distinguish package/module qualification, struct/class member access (.), or static member access (::).
Hm, you should really adopt more types of documentation. I find the tutorial very hard to follow, a language reference would be much more usable.
https://diataxis.fr/compass/
Note on example of UTF-8 strings. It's counting " has " in the length. You can change it to:
I’ll look into this
This compiles:
Which doesn't feel right.I also get a weird error message pointing into the stdlib trying to do this:
I assume because b takes ownership of s.bytes? Doing &s.bytes fixes it.The "Run Code" button une the exemple that take 2min to process is kinda funny for a langage comparing itself with C..
Broadly speaking, does Evergreen allow me to prove/enforce more invariants than what Verus/rust allows? Evergreen certainly looks cleaner since its built in rather than bolted on.
> More Powerful Than C. Safer than Rust.
This is an INSANE claim.
AI has really lowered the bar to allow people to create new languages from scratch. I'm not repulsed by AI generated output as others are, so my critique does not fall along those lines. Actually, I think that more people can do this now means the bar has risen for what we should expect from these languages and their authors. Before a spec and a prototype implementation, and a willingness to learn was enough, but today I don't think that's the baseline, not anymore.
I understand the author has posted this, and explicitly several times in the README and here on HN has said this is a sketch and is for learning purposes and experimentation. That's great and I support such efforts wholeheartedly. So my criticism is given in the spirit that this project can be significantly improved.
However, the LLM presentation means the author has cosigned statements I don't think they should be cosigning.
For example, your homepage makes some pretty outrageous claims: for a language that didn't exist before last week, you're claiming it is "more powerful than C" and "safer than Rust". There is very little here to support these claims, and I think they should be retracted.
First, how is this language more powerful than C and why can't C adopt what this language does? Why can't C use your technique as a framework / preprocessor and do exactly what Evergreen does? If it's technically possible for C to do all this I don't think you can claim Evergreen is more powerful.
Also, I don't see any benchmarks, maybe I missed them. How can you claim the proofs don't affect performance? You say that the proofs are erased after they're checked but that doesn't necessarily mean there's no performance cost for having to write the code a particular way. To credibly make this claim you'll have to show proof.
And please when you do the benchmarks, make sure the AI actually optimizes the baseline version. There was another AI-authored language posted here recently which also made similar grand performance claims, but they didn't make sure they were being fair in what they were comparing: https://news.ycombinator.com/item?id=50238979. The AI will show your language is faster than Rust or C or whatever by writing suboptimal Rust / C.
When you say it's safer than Rust, you're leaving out that your system is incomplete and can't handle some things that Rust already handles, like sync + send. Moreover, the claim seems to be the existence of the features in your language defacto make it safer than Rust, but again that's not proven. Do they really? Also, several times in the Readme you claim Rust can't do particular things, when it actually can, just not statically e.g. using Rc and Refcell. In another case I don't think you're aware of https://doc.rust-lang.org/std/num/type.NonZeroU64.html.
Is the claim you can do those things where Rust can't, or that you can do them statically where Rust can only do it dynamically?
Finally, for some of these examples they seem to take a very long time to check, despite being so small. The overflow example takes almost 10 seconds on my machine, it's only 9 lines of code. How does this scale to an entire program? What's the largest program you've written to test this?
Anyway, I'm not saying any of this to discourage you, just to say that you really can't make the claims you're making without proof, and it's not enough to say "well the AI made the website and it's prone to making overblown claims without proof" -- no, when you publish them, the AI's words are your words. You can stand by what you can prove but otherwise you should be careful making grand claims.
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.
Overflow is allowed. Overflow behavior is unspecified, like C++
Which contradicts the claim 'safer than Rust' given that in Rust it either panic or wrap.
If you want to assume that overflow wraps either:
Your hardware does this OR You implement it in software
Landing page says a lot of vibecoding involved…
So it's Rust with compile-time checks? So its just Rust? What can be done in this language that can't be done in Rust with a macro?
```
macro_rules! nonzero {
($n:expr) => {{
}fn main() {
};```
If you need something to be provably mathematically correct you should write it in Lean, or Coq, some kind of dedicated verification program, if you merely need to guarantee certain conditions at runtime, you can just write some macros! I understand that they want certain facilities like proof by induction, and the ability to prove arbitrary theorems but why would you do that when you can write it in a dedicated language (Lean/Coq) that has been around for a long time, with far more tooling?
That aside, I think Evergreen is still a nice language, and can have applications, its just the ecosystem around it that needs development.
It is different because for many cases you may need to prove your assertions. Consider:
fn foo(x: usize) -> NonZero where x != 5 { NonZero::new(x - 5) }
I do not believe this is achievable in Rust.