Since 2026/05/11 I have been massaging the output of #c2rust run on the #metamath source code into increasingly idiomatic #Rust. Right now verification of large databases of theorems runs in about 80% of the time of the C binary but I'm haven't yet converted all the IO away from stdio routines which want NUL-terminated CStrings (and the super unsafe *const u8). I've stripped out the idiosyncratic private memory management in favor of pre-allocating vectors and string buffers which is an improvement in performance and maintaining my sanity.

Played around with #c2rust to translate gwsh (a shell, a descendant from dash) from #c to #rust. Although I encountered two bugs, duly reported, where the generated code was incorrect, they required only small modifications, and after that, its translation of the shell was able to build successfully and pass all the tests I could think to throw at it.