I know many academics that exclusively use Haskell or even Idris and Agda which are even more obscure but more correct. Agda is so “correct” that the language

I know many academics that exclusively use Haskell or even Idris and Agda which are even more obscure but more correct. Agda is so “correct” that the language is total and not Turing complete with the exception of a “partiality monad” that allows for partial and Turing complete computations — similarly to how Haskell isolates effects on the world from the main language and encapsulates them into a special type, Agda isolates partial computations. And this language is very much used within specific academic fields.