Sorry you're getting downvoted but you're not alone, I have the same thoughts every time. I just knew bringing it up wouldn't be good. I could never have a verbal discussion about the language. I think that's the reason there's no GIS library written in Coq, even the most mature person couldn't hold back the giggles long enough to get anything done.