search

hmemcpy / milewski-ctfp-pdf

Bartosz Milewski's 'Category Theory for Programmers' unofficial PDF and LaTeX source
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Other
11.02k stars 595 forks source link

Consider Formally verifying the properties in Category Theory using proof assistants. #311

Open HaoYang670 opened 1 year ago

HaoYang670 commented 1 year ago

In the book, we have so many theorems and properties defined, which cannot be formally proved by Haskell or C++.

Is it a good Idea if we use proof assistants to prove these theorems, for example Coq, Idris or Agda ...?

BTW, I have started a project to interpret the book "conceptual mathematics" in Coq when learning category theory: https://github.com/HaoYang670/conceptual_mathematics