4 ms·
OK, but what kind of experience does Tao (I was actually well aware of who he was) have with programming and type theory in particular? By the way, is not the t
by dakimov 14y ago
OK, but what kind of experience does Tao (I was actually well aware of who he was) have with programming and type theory in particular? By the way, is not the type theory already a formalism? Cannot we construct formal proofs with it? Is it possible that he reinvents the wheel and describes a rather trivial thing in an overcomplicated roundabout way? Do you imply that a 'real' mathematical formalism is better than a formalism from the computer science? After all, equivalence is essential to mathematics, pretty everything can be represented and intuitively understood in a different equivalent way. This article is too long for me to crack it that fast, so maybe I am just not quite there yet in understanding.
- banachtarski 14y agoIt isn't a mathematical formalism. I have studied books on lambda calculus and all that. A computer scientist's understanding of what "well-defined" means is very different from a mathematician's. It's not to say that it doesn't work, just that the standard is very very different. The standard of well-definedness for a physicist and a mathematician is also very different. Example: compare what constitutes a "good enough" definition of a real number to these three disciplines.
- evincarofautumn 14y agoCould you elaborate on your perception of definitions of lambda calculus? Or, say, SK calculus. They’re very simple systems and entirely syntax-directed, so I’m curious to know where they “go wrong”—how would you prefer a definition be presented?