Interesting. Ever hear of the work of Jean-Yves-Girard? (You mentioned mathematical logic) I hear his book “The Blind Spot” is an excellent lecture on the nature of mathematical truth by a seasoned veteran of such difficult affairs.
I like Girard. The Rust programming language’s borrow checker probably wouldn’t’ve been invented yet if it weren’t for Girard’s 1987 paper, “Linear logic”. (The paper got sustained attention from numerous programming-languages researchers; I read many thousands of papers on programming-language design before the appearance of Girard 1987 and I can recall no exploration of the use of linear types, use-once variables or whatever you want to call them before Girard 1987.)
Yes, I have! Girard is very… opinionated, he is fun to read for that reason. That is, Jean-Yves has some spicy takes:
Quantum logic is indeed a sort of punishment inflicted on nature, guilty of not yielding to the prejudices of logicians… just like Xerxes had the Hellespont – which had destroyed a boat bridge – whipped.
I enjoyed his book “Proofs and Types” as an introduction to type theory and the Curry-Howard correspondence. I’ve looked through “The Blind Spot” a bit and it also seemed like a fun read. Of course, you can’t avoid his name if you’re interested in linear logic (as I currently am), since the guy invented it.
Interesting. Ever hear of the work of Jean-Yves-Girard? (You mentioned mathematical logic) I hear his book “The Blind Spot” is an excellent lecture on the nature of mathematical truth by a seasoned veteran of such difficult affairs.
I like Girard. The Rust programming language’s borrow checker probably wouldn’t’ve been invented yet if it weren’t for Girard’s 1987 paper, “Linear logic”. (The paper got sustained attention from numerous programming-languages researchers; I read many thousands of papers on programming-language design before the appearance of Girard 1987 and I can recall no exploration of the use of linear types, use-once variables or whatever you want to call them before Girard 1987.)
Yes, I have! Girard is very… opinionated, he is fun to read for that reason. That is, Jean-Yves has some spicy takes:
I enjoyed his book “Proofs and Types” as an introduction to type theory and the Curry-Howard correspondence. I’ve looked through “The Blind Spot” a bit and it also seemed like a fun read. Of course, you can’t avoid his name if you’re interested in linear logic (as I currently am), since the guy invented it.