I'm sure its technically possible, you might need to provide a bit more context if you expect anyone to change course here and port it to a programming language approximately no one has heard of rather than Rust though. What makes you think that would be a good idea?

I don’t think lean4 compiled code is as efficient as rust. For verification purposes, there are some tools allowing formal verification of rust code.

Never heard of it, and I nerd out on programming languages. Reminds me of a convo yesterday with my coworkers where I noted I never heard of Sheerpower a language someone who worked there had done, and I have heard of languages so old and niche most people are shocked.

My first programming interview my interviewer was like what the heck are you doing with D? And he noted he has a room full of devs where nobody knows what D is.