I learned coq as a teenager because the name was funny and one defined everything in terms of the `succ` function.

Never underestimate our motivation.

Continuing to do things only because they’re funny as an adult is one of life’s little treats!