3 ms·
I don't know, but Russel O'Connor got his PhD in 2008, the same year that type classes were introduced in Coq. There has been a lot of development on the Coq p
by fmap 9y ago
I don't know, but Russel O'Connor got his PhD in 2008, the same year that type classes were introduced in Coq.
There has been a lot of development on the Coq proof assistant since then. I don't imagine that working with Coq in 2008 was particularly pleasant. :)
- auggierose 9y agoI don't think working with Coq has ever or will ever be particularly pleasant :-) O'Connor gave a nice talk at TPHol's which I attended: https://arxiv.org/abs/cs/0505034 https://arxiv.org/abs/cs/0505034 Keeping up with Coq shouldn't have been too difficult for him.