> Idris's support for borrowing seems less powerful than Rust (it lacks first-class mutable borrows as far as I can tell). Depends on what you mean. Idris's no

> Idris's support for borrowing seems less powerful than Rust (it lacks first-class mutable borrows as far as I can tell). Depends on what you mean. Idris's notion of multiplicities essentially subsumes Rust's borrowing (there's some differences with affine vs linear types), so I can't think off the top of my head of things that you can ensure with Rust that you can't with Idris, but Rust has a lot more quality of life improvements that make things less clunky (also having a GC, Idris can get away with a lot less need for borrowing in the first place).