Comment by still_grokking
8 hours ago
Can someone ELI5 that for me?
Is this the mathematician's variant of "my language is better than your language", or what does this post actually discus? Something fundamental in the philosophy underpinning things or just the way to express them?
Paulson is a lead developer of Isabelle , a proof assistant that is not based on dependent types.
> Is this the mathematician's variant of "my language is better than your language",
Almost. A closer analogy is comparing paradigms, say OOP vs functional programming.
Isabelle is different from the big three - rocq. lean and agda. The latter three have propositions as types. The type of your function is the theorem statement. The function body is the proof. Isabelle works differently. Author makes a convoluted argument that (a) one doesn't have to stick to the currently popular paradigm and (b) in conjunction with AI, Isabelle offers distinct benefits.