Harry R. Schwartz

Code writer, sometime Internet enthusiast, attractive nuisance.

The author at the Palais du Luxembourg in Paris, November 2022. 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


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

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: