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.
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.
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.
That's basically SPARK (the Ada subset) but with c-like syntax (more or less).
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.