Kirby says: >I mentioned Robert's views specifically but only mentioned yours in passing in referring to computer science as some "bastard offspring" of mathematics (I left a footnote to that one).
Please! I said it was "pronounced a bastard by some of those in attendance". You have totally distorted my meaning here. In fact, I followed that immediately by the best reference I could (memory!) to a lovely fictional book about the time of the construction of the IAS computer. I passed that book onto someone and I really wish I could get another copy or at least remember the title. I was referring to the anti-machine attitude described in the book by some of the mathematicians at IAS at that time.
"After Goedel's famous results there developed a "schism" in mathematics when abstract mathematics and constructive mathematics became largely isolated from each other with the "abstract" steam growing into what we call "pure mathematics" and the "constructive stream" into what we call theory of computation and theory of programming languages. Univalent Foundations is a new area of research which aims to help to reconnect these streams with a particular focus on the development of software for building rigorously verified constructive proofs and models using abstract mathematical concepts. This is of course a very long term project and we can not see today how its end points will look like. I will concentrate instead its recent history, current stage and some of the short term future plans."
Sounds very interesting to me. If you don't like the sentiments ignore it. Most will.