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