Hi Anthony - very nice post - Can I ask you - when you write: "there are two major branches of dependently typed languages (and several minor ones), the "formal" type theories, such as Agda, Coq, Lean, Idris, etc., and the "semantic" type theories, being NuPRL and the more recent RedPRL."
This suggest there is something deeper to understand about Type Theory, beyond just the technical details. Would you mind elaborating a bit more why you think RedPRL is more "semantic" and less "formal" and/or can you maybe provide a link to an explanation providing some more background to this intuition?
thanks a lot,
Stefan
