Relatedly, at the Midlands Grad School 2019 conference, John Hughes did an introductory course to QuickCheck in which one of the final exercises (meant to demon

Relatedly, at the Midlands Grad School 2019 conference, John Hughes did an introductory course to QuickCheck in which one of the final exercises (meant to demonstrate the use of Haskell and QuickCheck to black-box test arbitrary binaries) was to model `fopen`, `fprintf`, `fclose` and friends in C. I never actually did it, but I guess that's one of the most comprehensive ways to find out how something behaves!