|
|
|
|
|
|
by BlanketLogic
55 days ago
|
|
|
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. |
|
|