Harry R. Schwartz

Software engineer, nominal scientist, gentleman of the internet.
Member, ←Hotline Webring→.

bearded cartoon drawing of the author hacker news gitlab sourcehut pinboard librarything 1B41 8F2C 23DE DD9C 807E A74F 841B 3DAE 25AE 721B


British Columbia






Recommended Reading from the DeepSpec Summer School

Recommended Reading from the DeepSpec Summer School

Published .
Tags: computer-science, math, formal-verification.

The first DeepSpec Summer School on verified systems is wrapping up. We’ve spent the last couple of weeks learning to use Coq to verify compilers, operating systems, data structures, and file systems.

We reached the consensus that Coq’s documentation isn’t as approachable as it might be. We’ve begun organizing an effort to improve it.

As part of that, we’re combing through our (extremely active) internal Slack group in preparation for publishing some of the tips and strategies we discussed and developed. I offered to clean up the #recommended-readings channel, where folks recommended papers and other readings that they thought might be of general interest.

Our main textbooks

You might like these textually similar articles: