As usual with such provers the model is fairly constraining. But nowadays it seems to start being usable in more cases. Deriving the Lean code from the source code is nice too.
It's indeed not urgent to have this language feature in Rust. I'm less convinced about the case put forth regarding function overloading not being necessary though. Feels a bit like post-hoc justification in this case.
This is indeed an important pattern to build reliable systems. It's worth exploring in various languages. Here is the Rust perspective.
Probably more than you think in this setup. And even more in C++ with the STL having years of smart tricks behind it.
Bad actors clearly want to compromise supply chains. Stay safe and keep your eyes open.
Interesting exploration of how static and dynamic dispatchs work behind the scene in Rust. The chosen tradeoffs are different than in C++ and that's something to keep in mind.
Comparison of two concurrency models. This is a light read which shows quite well the differences.
Interesting case where you want to property test but without a specific property base test tool. Indeed, if you need to be exhaustive and the input space is small enough this is the better decision. This article also comes with interesting point on Rust type system but that's less central to the main point.
Unsurprisingly it's not all unicorns and rainbows. This piece tries to highlight the right questions to ask yourself before aiming for a rewrite.
Interesting tool. Maybe more chances for C++ and Rust hybrids?
Interesting policy. I think it strikes a good balance.
More ideas of things to check to harden a service, goes beyond just what's deployed. Many good points on how to handle errors and such.
Good checklist to reduce your attack surface as much as possible when deploying your service.
While some rewrite from Zig to Rust... others follow the opposite path. This is an interesting read pointing the strengths and weaknesses of both ecosystem. There's no one size fits all in our field so it's important to have this kind of explorations.
Another attempt at easing the pain navigating the Rust crates ecosystem? It has its merits as well.
A nicely balanced view at Rust the language but also the ecosystem. It's not all pretty and real issues are looming.
Still need some work I'd say but this is interesting research. Transpiling C++ to Rust is getting more accessible. It need some improvements on the optimisation side to be more generally usable.
Interesting Rust options to limit the amount of heap allocations if you're constrained by memory or for performance reasons.
Friendly reminder that the answer is "no". You don't want to just rewrite everything, it's not just a syntactical translation, it's a long project and at best you tackle critical components.
Sounds obvious to me, but I guess it's worth repeating. It illustrates well the type of issues you still have to deal with in multi-threaded Rust.