5 ms·

Would you mind suggesting an introductory text for this stuff?

• auggierose 7y ago
  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.
• sasaf5 7y ago
  Tutorial on CoQ, a proof assistant https://news.ycombinator.com/item?id=21185624 https://news.ycombinator.com/item?id=21185624
• Koshkin 7y ago
  https://mitpress.mit.edu/books/little-prover https://mitpress.mit.edu/books/little-prover
  • faizshah 7y ago
    Great recommendation, thanks!