5 ms·
I think we can forgive such stuff at least in the intro. This document is clearly an introduction to type systems for people who know more about programming th
by adrianratnapala 9y ago
I think we can forgive such stuff at least in the intro. This document is clearly an introduction to type systems for people who know more about programming than they do about the underlying maths and logic of type theory. Good.
Also good is that it starts from what the reader knows informally rather than trying to build everything rigorously from the ground up.
- catnaroek 9y ago> Also good is that it starts from what the reader knows informally rather than trying to build everything rigorously from the ground up. It's certainly pragmatic, but is it good? Maybe I'm biased as a math student, but I've seen first-hand the horrors that happen when people think they know something just because they have a vague intuition about the topic's main ideas.
- adrianratnapala 9y agoBut whenever I have learned maths in strict lemma-proof form it was on the second time around. That is, I first had a general sense of the field and intuition about concepts and some of the results, and then rigorous stuff makes sense. From everything I've read about how mathematicians work, I thought that was normal.