As I've been working on my website, I've noticed there are a whole bunch of non-obvious constraints for what makes valid HTML. This of course makes me think about formalizing the HTML spec in Lean (or something).
Someone please tell me this is a terrible, horrible, no-good idea.