Yet another Hacker News

Evergreen: A Provably Safe Systems Language

48 points jordan_bonecut 1 hour ago 27 comments

jordan_bonecut 1 hour ago | parent

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!

sblom 1 hour ago | parent

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.

jordan_bonecut 1 hour ago | parent

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.

0c3ca83 21 minutes ago | parent

It's so strange how much effort goes into producing a language that people don't even intend to write.

gchamonlive 14 minutes ago | parent

[delayed]

jeremyloy_wt 13 minutes ago | parent

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.

TofuLover 1 hour ago | parent

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

jordan_bonecut 1 hour ago | parent

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.

nicce 1 hour ago | parent

> 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.

jordan_bonecut 52 minutes ago | parent

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

0c3ca83 19 minutes ago | parent

And what about allocations and threads?

jordan_bonecut 14 minutes ago | parent

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

tancop 16 minutes ago | parent

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?

throwaway17_17 54 minutes ago | parent

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.

throwaway17_17 1 hour ago | parent

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.

jordan_bonecut 57 minutes ago | parent

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.

ch4s3 55 minutes ago | parent

How long have you been working on this?

jordan_bonecut 48 minutes ago | parent

I have been building little prototype languages for years. This iteration which is heavily AI powered is a couple weeks old

ch4s3 39 minutes ago | parent

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.

ch4s3 56 minutes ago | parent

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/

gtutino 1 hour ago | parent

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

LiamPowell 11 minutes ago | parent

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?

skybrian 1 hour ago | parent

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.

jordan_bonecut 58 minutes ago | parent

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

skybrian 46 minutes ago | parent

Yeah, if I were motivated I’m sure I could figure it out from the tutorial.

jordan_bonecut 25 minutes ago | parent

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

kreco 5 minutes ago | parent

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)