The Coq mailing list

[Hugo Carvalho <hugoccomp AT gmail.com>]

Thanks!

I had heard of the Odd Order Theorem formalization, but always assumed it followed a paper (with ad-hoc proofs of elementary statements, taken from whatever references as needed), not an actual (pair of) textbook(s). And some fairly advanced ones, at that! I'll be sure to check it out. I guess i'll also have to give ssreflect tatics a chance... (i don't even know anything about them, i'm just scared of change; but come on, CPDT/Chlipala-style code just seems so much cleaner (even if i'll never be smart enough to reproduce it))

The HOTT book is just delightful, isn't it? I hope we see more books written in this collaborative, in-the-open, formalized style. But come on! It's type theory, that's, like, the one thing i would expect Coq to excel at formalizing! That's cheating! :)
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)

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?