Post #1985136
2026-04-25 11:38 UTC
@AmenZwa A debate about Lean. Paulson is the creator of Isabelle. Many historical views inside.
https://mathstodon.xyz/@Jose_A_Alonso/116461246243925593
Replies (1)
-
@AmenZwa@mathstodon.xyz 2026-04-25 15:17
@fl@mathstodon.xyz @Jose_A_Alonso@mathstodon.xyz I have long been an admirer of Paulson’s work, decades long, in fact. He wrote my favourite programming book on my favourite programming language. So my views maybe biased in Paulson’s favour. Having said that, I agree with his position, specifically about the cultism surrounding Lean—it’s mathematicians’ Python. On the other hand, cultism does not automatically negate the intrinsic value of Python and Lean. No matter the momentum, we each make exercise our independent judgment. That is why I’m with Paulson. PS: I am a staunch Agda fan.