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.)

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?

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

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

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

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.

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.

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.

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

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

(never tried either tho)

You mean @Jonathan Sterling

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.

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