Comment by raphlinus

Of the things I'm familiar with that are out there, this looks most familiar to Idris 2. Also, while Lean is primarily used for mathematical proofs, Lean 4 is beefing up its capabilities to be used as a regular programming language as well. Can anyone speak to the differences between this and those?