You have a misinformed view of what a "computer scientist" is; I have never written a Coq proof, but I think my publication record buys me the label "computer s

You have a misinformed view of what a "computer scientist" is; I have never written a Coq proof, but I think my publication record buys me the label "computer scientist". (I recognize you were probably usually your specific examples as examples of a kind, but it's that kind which I think is misinformed. You probably think a "computer scientist" must necessarily be a theoretician, which is not the case.)