3 ms·
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.
by ogogmad 5y ago
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.
- wlib 5y agoI’m aware of math being entirely useful outside of programming - my little rant is more about how little programming is inspired by math
- exdsq 5y agoI'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.
- black_knight 5y agoWhile 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/pdfs/Constructive-mathematics-and-computer-programming-1982.pdf https://raw.githubusercontent.com/michaelt/martin-lof/master...