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.

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

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