[ogogmad]

Type theory has uses outside programming. It can be used to make constructive logic rigorous, which was in fact Martin Lof's original use for it.

[black_knight]

While making constructive mathematics rigorous was Martin-Löfs original goal, he was quite early aware of the applications to computer science. See for instance his 1979ish paper «Constructive Mathematics and Computer Programming»[0]

[0]: 1982 version: https://raw.githubusercontent.com/michaelt/martin-lof/master...

[wlib]

I’m aware of math being entirely useful outside of programming - my little rant is more about how little programming is inspired by math

[exdsq]

I've used Haskell for 18 months in a professional setting. I prefer C++. Grass is always greener - having endless abstractions to be mathsy becomes a real pain when you're trying to build real products.