> it's useful to have a strong advocate for the minority view that ML was on the better track. Total agreement here. I also really enjoy his rather principled,

> it's useful to have a strong advocate for the minority view that ML was on the better track. Total agreement here. I also really enjoy his rather principled, HoTT-inspired perspective on type theory. I vastly prefer PFPL to Pierce's TaPL due to PFPL just being less preoccupied with the diversity of reasoning possible and more interested in explaining the "one right way" efficiently.