[nodogoto]

What's not mentioned in the comment you're replying to is the postgraduate-level type theory you need to learn and constantly refine to work with these languages at a practical level. So be aware that even if you put the time into learning them, it's unlikely you'll get to use them at work.

Look up Coq, Agda, Lean, and Idris. I would start with Coq, it's the most used. Idris is more like Haskell and programmer-oriented.

Edit: Nevermind, apparently they were just talking about Haskell...

[formulathree]

I'm more thinking in terms of logical primitives for the design of modules and components that can be composed, decomposed and recombined. I'm thinking less about proof based correctness.