3 ms·
Mathematical Components for the Coq system
- dwheeler 10y agoCool. People interested in formalized math might be interested in metamath: http://us.metamath.org/index.html http://us.metamath.org/index.html or one of several other systems; here's a list of some and what they've proven: http://www.cs.ru.nl/%7Efreek/100/ http://www.cs.ru.nl/%7Efreek/100/
- fmap 10y agoThis is a wonderful book and I recommend it to anybody learning Coq. The mathematical components project has made (and continues to make) great strides when it comes to formalizing research level mathematics. Before this book, there was only a small manual for ssreflect and information scattered throughout a dozen research papers. It's good to finally see more of a focus on documentation, since there are many people in the community who could benefit from using mathcomp instead of developing their own implementation of common mathematical structures.
- mrcactu5 10y agoMicrosoft is kind of like McDonald's. If I want a decently cooked burger I should cook it myself. If I am totally unfamiliar with an area, I go to McDonalds. I expect a certain minimum from Microsoft and the book exceeds that. Also UPenn's Software Foundations is written in CoQ https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html