@liamoc @jonmsterling I had to sit down and watch some of Dr Buzzard's earlier talks around 2019, and he does just blatantly lie about Isabelle and Coq ("They don't have unicode! Setoid hell! Isabelle doesn't have quotients!" etc. etc. etc.).
I had happily forgotten how jarring it all was; I had also forgotten how many people had pointed and patiently explained to Dr Buzzard how what he was saying was wrong, only for Dr Buzzard to continue the same talking points in every talk he gave.
If we charitably call this "motte-and-bailey" or "strong claims", then we might as well be equally charitable with this rubbish book. (And we really shouldn't be charitable with this book, I just think people are having double standards here for inexplicable reasons.)
@thmprover @jonmsterling Sorry, if this is a reply to a previous toot, would you mind sending me the link? I'd like to follow up on the context, but Mastodon doesn't seem to be loading previous messages. If your toot was meant to be standalone, what book are you referring to?
@thmprover @jonmsterling I see, thank you very much.
@ayhon @jonmsterling This book "The Proof In The Code" by...some random guy...prompted Jon Sterling's original post:
https://www.quantabooks.org/