You'll have to ask Jon about what "idea" Nuprl's intrinsic untypedness is "not an essential part of". I'd say the most important thing about Nuprl is dependent refinement typing. In particular, Nuprl is extrinsic dependent typing, since the intrinsic type system is trivial. That turns out to be very interesting too, but makes the approach less broadly applicable.

I have some outlandish views about Nuprl. I don't consider its PER semantics to be a model, in the usual sense of model theory. It's proof-theoretic semantics. It's a semantic justification of some proof principles. Kind of like a strong normalization proof for ITT. You can point out that it's technically a realizability model. But I'd say that's because the terms are realizers. *What are they realizing?* That would be a model. The model theory of Nuprlish systems is currently virtually nonexistent. Somebody ought to fix that. There's a set-theoretic semantics (actually two, and they are different... sort of) for an old version of Nuprl. That's it, AFAIK.

On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman wrote:

FWIW, I think the only thing I have against NuPRL "in principle" is
that it seems to be closely tied to one particular model, which is the
opposite of what I want my type theories to achieve.  I say "seems"
because then someone says something like Jon's "Nuprl's underlying
objects are untyped -- but that is not an essential part of the idea",
providing an instance of the problem I have with NuPRL "in practice",
which is that every time I think I understand it someone proves me
wrong.  (-:O

Can you explain the difference between "definitional" (whatever that
means) and "strict" equality in Andromeda?  Of course there is the
technical difference between judgmental equality and the equality
type, but that doesn't seem to me to be a "real" difference in the
presence of equality reflection, particularly at the purely
philosophical level at which a phrase like "equality of sense" has to
be interpreted.  As far as I know, even beta-reduction has no
privileged status in the Andromeda core -- although I suppose
alpha-conversion probably does.