Hacker News new | past | comments | ask | show | jobs | submit login
Mathematical Components for the Coq system (math-comp.github.io)
106 points by colinprince on Dec 28, 2016 | hide | past | favorite | 3 comments



Cool. People interested in formalized math might be interested in metamath: 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/


This 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.


Microsoft 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




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: