Formal Methods

166 readers

3 users here now

founded 1 year ago

MODERATORS

Ategon

synthetic_apriori

So you want to be a proof engineer? (proofcraft.org)

submitted 1 year ago by synthetic_apriori to c/formal_methods

1 comments fedilink hide all child comments

you are viewing a single comment's thread
view the rest of the comments

[–] armchair_progamer 3 points 1 year ago* (last edited 1 year ago)

The article skipped the most well-known and important books! (at least from my circle)

Software Foundations: https://softwarefoundations.cis.upenn.edu/

Certified Programming with Dependent Types (CPDT): http://adam.chlipala.net/cpdt/

I recommend reading the first before the second, although sometimes pages from CPDT show up in Google when you have a question. Also don't hesitate to check out the Coq reference manual (https://coq.inria.fr/distrib/current/refman/), although it will be overwhelming at first since it's very pedantic and detailed, it becomes very useful once you have a basic understanding of Coq (like from reading the above).