Agreed!; Personally, I am of the opinion that Idris for one is mature enough that there is no need to forego tools that have a proper proof system for the entire program. It’s feasible today.

Idris is carefully and purposefully described by its creators as not production ready. Nonetheless, because of what Idris is, it’s arguably more production-ready than languages which don’t even attempt formal soundness to anywhere near the same degree. In other words: Idris is not a complete Idris. But! All the other languages are even less complete Idrises!

Big old “personal opinion” disclaimer here though. –Let’s prove it’s not possible to use Idris by doing it! Shall we?