I'm really hopeful that Julia will continue to gain adoption.

That said, I would love to have good data science library support (bindings to stuff like BLAS/LAPACK, Torch, Stan, etc) in Idris.

Imagine vector and matrix dimensions checked at compile time. Probabilities guaranteed to be between 0 and 1, checked at compile time. Compile-time enforcement that you are handling "nil/null" data inputs correctly when reading data from a database or CSV file. Writing a web scraper with linear types to help catch bugs & performance leaks. Maybe even proving theorems about the math code you're writing ("is this a valid way to express X"?).

Maybe not ideal for rapid exploratory model development, but it'd be pretty damn cool for writing data science tooling/libraries and "production" ML code in my opinion.

Not that it has bindings to other tools, but it sounds like Dex[1] would be relevant to your interests!

[1]: https://github.com/google-research/dex-lang

Looking forward to Dependent Haskell for linear algebra, and seeing what existing stuff can be retrofit.