The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Altough now i wonder just how difficult would be to formalize Benjamin Pierce's "Types and Programming Languages"... (and also wonder if i'll ever get around to start reading it seriously)

Software Foundations goes some distance in that direction, but dealing with variable binding in a way that doesn’t get too heavy for a book intended for teaching is a significant challenge.  By stopping at simply typed systems, I was able to use the trick of only considering substitution of closed terms, which streamlines things quite a bit.  

    - Benjamin

If anyone cares, here's why i asked this question. I've read somewhere that one of the challenges proof assistants face is to be convenient/useful enough that they get regularly used by mathematicians, as right now they require too much specialized training. My train of thought was simply "Well, maybe they can't be used in the day-to-day work, proving cutting-edge theorems. But perhaps a few undergraduate textbooks have been formalized, showing that it is possible to use a broad range of introductory mathematical reasoning within proof assistants?".
And to clarify, i know you can reason with math in a proof assistant, it's kind of the whole point of the ordeal, but i assume that textbooks, in addition to explaining whatever their topic might be, also show by example how to compose proofs about the subject, in a way that's useful to a mathematician for their whole career. So if you show how to replicate the usual textbook within a proof assistant, you've shown how to do a fairly general amount of math within a proof assistant.
Of course, this is all quite optimistic. Maybe the usual way of doing math just isn't going to convince a computer, and we're going to need a radically new kind of way to do it, instead of building blocks that eventually lets us do math the old-fashioned way (except in a checked environment).

2014-08-13 16:35 GMT-03:00 Harley D. Eades III <harley.eades AT gmail.com>:

Hi, Hugo.

The Homotopy Type Theory book is a nice example.  It can be found here:

http://homotopytypetheory.org/book/

A large portion of the book was formalized as it was written.

Very best,

.\ Harley

On Aug 13, 2014, at 3:01 PM, Hugo Carvalho <hugoccomp AT gmail.com> wrote:

I'm curious to know if there have been efforts towards a full formalization of any textbook. I do know of the few books that have accompanying Coq code (Software Foundations, CPDT, Coq'Art). but i'm more interested in knowing if there is a textbook that was given a formalization after-the-fact (but then again, a textbook written from the ground-up with formalization in mind is also an interesting project, even if for different reasons).

It seems to me that, outside of "pure Computer Science" topics (such as programming, languages, algorithms), the most adequate topic for such a textbook would be math; logic and discrete math, specially, but other math topics also seem plausible.

Does the Club know of any pointers in this area?