I still want to try the ZZ language (https://github.com/zetzit/zz https://github.com/zetzit/zz) someday. It compiles to C, and uses a SMT solver to prove that y

I still want to try the ZZ language (https://github.com/zetzit/zz https://github.com/zetzit/zz) someday. It compiles to C, and uses a SMT solver to prove that you don't index out-of-bounds at compile time. But I don't like how it lacks generics, uses C idioms, and compiles to C.