Is Martin-Lof's type theory foundational for stuff people are using today? Or is it an interesting idea that never came to fruition?
grumpymuppet 22 hours ago [-]
If you are interested in programming language theory (think language design) then, yes. In some sense, this kind of stuff is impossible to avoid.
If you're an engineer focused on shipping product, probably not. It's not TERRIBLY useful for most day to day coding tasks.
I would argue some understanding of theory is absolutely necessary if you want to make any significant tide change in CS. It's just that most people won't (myself included).
wduquette 17 hours ago [-]
Oh, I get the importance of type theory in general. I hadn’t run into Martin-Lof before.
grumpymuppet 7 hours ago [-]
Ahh, sorry, yeah. This stuff is classic. "Old" even.
deterministic 18 hours ago [-]
Martin-Lof's type theory is the foundation (or inspiration) for quite a few modern proof assistants. It is also an elegant non-set based foundation for constructive mathematics.
wduquette 17 hours ago [-]
And there it is. Thanks very much!
Rendered at 19:54:04 GMT+0000 (Coordinated Universal Time) with Vercel.
If you're an engineer focused on shipping product, probably not. It's not TERRIBLY useful for most day to day coding tasks.
I would argue some understanding of theory is absolutely necessary if you want to make any significant tide change in CS. It's just that most people won't (myself included).