I'm currently writing such a language myself in pure Lean, based on adjoint logic -- as well as graded modes and effects. I started by just trying to formally

I'm currently writing such a language myself in pure Lean, based on adjoint logic -- as well as graded modes and effects. I started by just trying to formally verify a Rust-like borrow checker and at this point I have a working interpreter and LLVM compiler and a formally verified kernel. All type checkers are theorem provers, btw, that's just Curry Howard. The question is exactly how expressive they are.