Yeah tom7 did a video on ‘badness’ in TeX: www.youtube.com/watch?v=Y65FRxE7uMcI am learning ins-and-outs of TeX because I am implementing it in OCaml. btw, tom7 is a really stand-up fella. His thesis on “Modal types for Mobile Code” seems very interesting. He mentions it in the video. This is the thesis: www.cs.cmu.edu/…/modal-types-for-mobile-code.pdf
(mobile code is ‘network’ code, basically JavaScript – Tom’s work, I believe, is concerned with formal verification of web code – if you are a webdev, read it!)