Stream: Miscellaneous

Topic: Nuprl


view this post on Zulip Patrick Nicodemus (Apr 08 2023 at 21:18):

How active is the research community around nuprl?
I cannot find much activity. Mark Bickford wrote a paper on formalized in Nuprl last year.
If I want to talk to people who regularly use Nuprl, what's the best discussion forum for that?
(I don't want individual names and email addresses. If the best thing available is to communicate with scattered individuals then this is not what I would call a thriving research community.)

view this post on Zulip Patrick Nicodemus (Apr 08 2023 at 21:21):

There is a follow up question.
It seems like nuprl is close to dead, although I could be wrong about this.
If so, why? Why hasn't extensional type theory received much research attention?
Frankly extensional equality seems much more practical for theorem proving even if undecidability of definitional equality is a hard pill to swallow and carrying around "proofs that proofs are proofs" is inelegant.
Lean has already given up this decidability of definitional equality and many mathematicians are using Lean. So... why aren't more mathematicians using Nuprl?

view this post on Zulip Patrick Nicodemus (Apr 08 2023 at 21:23):

Lawrence Paulson mentions the same thing here. https://lawrencecpaulson.github.io/2022/11/23/CTT_in_Isabelle.html

view this post on Zulip Karl Palmskog (Apr 08 2023 at 21:32):

last I checked, the only way to access Nuprl in practice was through some remote session (no local install)

view this post on Zulip Karl Palmskog (Apr 09 2023 at 10:18):

I did try to see if the Coq formalization of Nuprl could get some collaborative maintenance and dissemination, but no luck: https://github.com/coq-community/manifesto/issues/60

view this post on Zulip Pierre-Marie Pédrot (Apr 10 2023 at 08:24):

NuPRL as a proof assistant is a weird beast I never quite understood. As a realizability model, you need not only one but two proof assistants. One for the surface language (i.e. "the real NuPRL") and one for the metatheory (which is never quite specified). Also, the internal logic depends on the metatheory, e.g. Markov's principle in the NuPRL Coq implementation relies on additional Coq axioms. All in all this looks like adding a layer of complexity over an already existing proof assistant, which doesn't seem to be very practical.

view this post on Zulip Andrew Hirsch (Apr 10 2023 at 13:08):

I think Nuprl is dead now that Bob Constable has officially retired. They were talking a big game about distributing VMs (since it won't run on anything modern), but afaik that never actually happened.

view this post on Zulip Karl Palmskog (Apr 10 2023 at 13:13):

from what I understand, the Coq formalization could be extracted and run to some extent. That might be a way forward, but I guess in the end completely up to Rahli & Bickford. They'll probably also keep it [the non-Coq implementation] running inside Cornell for quite a while even after Constable's retirement.

view this post on Zulip Karl Palmskog (Apr 10 2023 at 13:21):

I heard anecdotes that formalizing large-scale math and big programs in the Nuprl system was significantly harder than in other comparable system (Coq, Isabelle, etc.). But hard to say whether the small userbase is due to this or the lack of an easy-to-build software distribution

view this post on Zulip Paolo Giarrusso (Apr 10 2023 at 14:08):

I've seen both the VMs online, and Jon Sterling's reimplementations

view this post on Zulip Paolo Giarrusso (Apr 10 2023 at 14:08):

(never tried either tho)

view this post on Zulip Bas Spitters (Apr 11 2023 at 14:42):

You mean @Jonathan Sterling

view this post on Zulip Andrew Hirsch (Apr 11 2023 at 15:49):

Karl Palmskog said:

I heard anecdotes that formalizing large-scale math and big programs in the Nuprl system was significantly harder than in other comparable system (Coq, Isabelle, etc.). But hard to say whether the small userbase is due to this or the lack of an easy-to-build software distribution

It was both. Nuprl was/is really hard to use, for seemingly fundamental reasons. But it was almost impossible to get access to it anyway unless you were physically at Cornell, which limited your options pretty severely.

view this post on Zulip Karl Palmskog (Apr 11 2023 at 15:53):

James Wilcox told me he was able to use it via SSH remotely a bit. But from what I remember he confirmed the general story of difficult-to-use software.


Last updated: Nov 29 2023 at 21:01 UTC