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.