Evergreen: A Provably Safe Systems Language

jordan_bonecut

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!

TofuLover

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

gtutino

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

skybrian

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.

kreco

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)

solatic

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.

RemingtonDavies

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.

irq-1

Note on example of UTF-8 strings. It's counting " has " in the length. You can change it to: let l = text.len(); text.push_str(" has "); text.push_usize(l);

sharifhsn

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.

rsrsrs86

Landing page says a lot of vibecoding involved…

LoganDark

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/

MichaelNolan

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.

ModernMech

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.

Magicrafter13

> More Powerful Than C. Safer than Rust. This is an INSANE claim.

heavensteeth

This compiles: type NonZero = usize where self != 0; fn main() -> NonZero { let my_nonzero = NonZero(1); my_nonzero - 1 } Which doesn't feel right. I also get a weird error message pointing into the stdlib trying to do this: fn main() { let s = std::string::String::new(); let b = s.bytes; s.len(); } I assume because b takes ownership of s.bytes? Doing &s.bytes fixes it.