You (rightly, I think) place Idris (and Agda, although that's more a proof assistant than a PL) beyond the reach of the average developer, and also, apparently, Haskell -- arguably a simpler language than Rust, but never mind -- but not Rust. And that's my point and, I guess, our point of disagreement. If you think that, on that spectrum between, say, Python and Idris, Rust is at a good level for the average application developer to the point where maintaining high-level applications written in Rust would ever be cost effective, then I think you are out of touch with the realities of the software industry and the economic forces that shape it. I thought the exact same thing as you twenty five years ago: C++ was obviously the right language for the average developer -- even more so than, I don't know, Delphi or Visual Basic -- wasn't it?

> What's a better general-purpose language for this mythical "average" developer?

I don't believe any low-level language will be cost-effective for application development for the foreseeable future, if ever, and the average developer is anything but mythical (I mean, embodied as a single person, perhaps, but I'm talking about teams).

> Rust has the same level of memory safety

It doesn't (due to much more prevalent reliance on unsafe as well as FFI), but that's very much beside the point because, as you acknowledge, safety is not what it's about.