|
|
|
|
|
|
by stepchowfun
1441 days ago
|
|
|
Coq is so much fun. It makes writing proofs feel like playing a video game. I've just finished writing a Coq tutorial [1] that is aimed at programmers (rather than, say, computer scientists). It covers topics like programming with dependent types, writing proofs as data, universes & other type theory stuff, and extracting verified code—with exercises. [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor... |
|
|