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?
Just cause it isn't used for webshit doesn't mean "approximately no one" has heard of it.
Lean is pretty much the most popular language mathematicians use today for computer-assisted proofs. More mature audiences may know about Rocq, Isabelle, etc., but Lean was already popular enough for a few people I know to have written their PhD theses on it about a decade ago.
I think GP is joking about a port to Lean because that would at least produce a formally verifiable output.
Oh, PhDs, you're right, that's not approximately no one... It's probably approximately one.
I like Lean (and more generally dependent types) but ffs Lean has a very, very small userbase for a project like this. GGP would have to really justifyv the benefits for such a switch.
Apparently roughly ~150k math PhDs live on earth right now, assuming they all know Lean that's between 0.001% and 0.002% of earth population so quite closer to no one than one
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.