Hacker News new | past | comments | ask | show | jobs | submit login

Would you mind suggesting an introductory text for this stuff?

Great recommendation, thanks!

Kind of embarrassing, but I cannot! The thing is, development of mechanised theorem proving has been driven by computer scientists, so proving program correctness, doing programming language semantics, and explaining constructive ideology is at the heart of most introductory text books.

I would recommend just following the "Theorem Proving in Lean" book for starters.

Tutorial on CoQ, a proof assistant


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