4 ms·

"Set theory is the 'assembly language' of mathematics. Type theory is the 'functional language' of mathematics."

• jonnybgood 10y ago
  According to who? I don't think that's a very good analogy. I think it's better to say type theory is just another language in a 'family of assembly languages'. Its superiority is very debatable and not commonly accepted as a foundation.
  • fmap 10y ago
    I think it's a nice analogy. It's a bit tongue in cheek, but it does give you the right idea when you compare it to programming languages. Set theory is a reductionistic system. It's supposed to give a foundation which is as "small" as possible. In set theory you start with almost nothing and you have to encode all useful concepts into sets before you can start proving/programming. Compare this to Turing machines, where you start with a very primitive model of computation. The first step in most treatments of Turing machines is similar to set theory, you show that some useful concepts (associative memory, high-level control flow, etc.) can be encoded into Turing machines. You then use this encoding to construct arbitrary programs. Type theory starts out with a functional programming language and you derive new concepts from free constructions. In type theory you shouldn't be encoding things at all. You should be describing concepts (~adding an API) and possibly extending your model (~the compiler). As analogies go, I'd say that this one is pretty accurate.