Asuran is an encrypting, authenticating, deduplicating archiver with a focus on saftey, correctness, and speed.
Asuran consists of several components, and is currently early in the process of being rewritten from Rust to Idris 2.
As I have grown more experienced with Rust, I have grown less and less excited about using it for large or security sensitive applications. It is a fine language, and certainly a step up from C/C++ in terms of usability. But even so, I've found myself constantly bonking into situations where the type system isn't quite powerful enough to express what I want in an ergonomic and non-footgun prone way. Dependent typing provides another layer of expressiveness that's honestly hard to describe to someone that's not tried it out, allowing much more expression of logical and security constraints within the type system.
I've grown fond of Idris, and I really want it to be a thing, so I've decided to take a gamble and have an experiment writing some serious systems software in a dependently typed language, possibly even doing a bit of integration with Rust.