Comment on Coq 8.13parentComments−mncharity5yThe 6.822 page[1] has a draft[2] of Adam Chlipala's "Formal Reasoning About Programs", "introducing both machine-checked proof with [Coq] and approaches to formal reasoning about program correctness".[1] https://frap.csail.mit.edu/main [2] http://adam.chlipala.net/frap/frap_book.pdf
Comments
The 6.822 page[1] has a draft[2] of Adam Chlipala's "Formal Reasoning About Programs", "introducing both machine-checked proof with [Coq] and approaches to formal reasoning about program correctness".
[1] https://frap.csail.mit.edu/main [2] http://adam.chlipala.net/frap/frap_book.pdf