On: The Little Prover

[JadeNB]

I think WaxProlix (https://news.ycombinator.com/item?id=9553471) was avoiding puerile jokes about (a homonym for) Coq, not avoiding Coq itself.

[WaxProlix → JadeNB]

Yes, exactly, especially in the context of "my girlfriend and I", "playing with", etc. Low-(brow|hanging fruit), even for me.