This is a tough sell. Yes, those languages (with some small nits about Ada) can accomplish the same safety guarantees, but they're nowhere performant enough in practice or memory efficient compared to Rust. A big part of the original mission of Rust was safety without performance compromises which for the most part its accomplished, though the price is paid during compilation. Further, their runtimes and limitations make it difficult to work directly with operating systems or low level system hardware. And I say this as someone who has written Haskell code in production.

That said, I would love for Idris to continue to develop. I'm a big believer in dependently typed languages and would actually improve correctness, assuming there are reasonable ways to avoid the other trappings of the language.

"but they're nowhere performant enough in practice or memory efficient compared to Rust."

I would not include Ada, if you're benchmarking against Rust. Mostly because Ada either outperforms it (because it can reduce sizes in the optimiser), or it is equal to it.

One of the big learnings from 3.8 27b is adding reasoning budget really hurts the model. you need to let it spin for as many thinking tokens as it wants to to get it out. Another big takeaway is reasoning effort set to low doesn't save you tokens: low is pretty uncertain about things so it ends up thinking more (you can find some tests from folks on youtube). The final question, as always, is what quant are you running it at? KLD matters _a lot_ when it comes to its performance and it especially manifests with MTP/DFlash acceptance rate which makes those long thinking traces take a long time.

It literally ran forever without a reasoning budget. I tried even the 2T model and cut it off after a half hour. This is to review a few hundred-line source file. It was consistent behavior from 2T to vanilla 27B to my ablated distilled version.