I'm hardly an expert on these sorts of philosophical questions. On the specific phrasing of "semantic" vs. "formal", I just copied the way it's explained in some of the works on computational type theory I read. I honestly don't even remember which term is for what at this point as I didn't think it was that important. I did not think anyone, much less an actual type theorist like Altenkirch, would find the terminology offensive. I'm not convinced he's right in calling it a "slur" (I can't even tell which of the two adjectives is supposed to be the negative one), but I'll respect his opinion.
I can, at least, give a contrasting viewpoint as I disagree with the idea that types should be considered fundamental (of course, I'm not a type theorist, so don't take my opinion as expertise).
My main intent in making the distinction was drawing a clear line between CTT-like systems which allow one to implement a type theory after you already have a working notion of computation (in this case, the untyped Mathematica/Wolfram Language), vs. more conventional type theories which have intrinsic notions of computation built-in, usually some extension of the lambda calculus. While the latter is nice, it doesn't help if you want to give an already existing system a way to reason about behavior. Of course, there are options outside of type theory, like what Isabelle/HOL or TLA+ do, but a type-theoretic approach requires less infrastructure and has fewer diversions/redundancies as some approaches based on embedding programs into a larger system. That has more appeal to me as a programmer, but there are, perhaps, other things worth caring about.
On a practical level, I think it's important to acknowledge that we can treat type systems in much the same way we treat unit testing. We can implement such systems as libraries; we don't need a static type checker as part of the compiler. To that end, a realizability-like approach (but not necessarily a PRL-like one) is a better fit for such projects than a system where we have to hack all our programs into a format that some intrinsic type theory might want. Lambda expressions and combinators are nice, but I'd like the option to reason about other things just as easily if I want without inventing a new system every time.
On a more philosophical level, it's important to note that the real world, in so far as any of it can be interpreted as some computational substrate, is intrinsically untyped. Any real instantiation of either computation or type-theoretic reasoning must be done using the same stuff following the same rules. In the real world, there can be no distinction on a fundamental level between the stuff of types and the stuff of terms. Either define type theory so that it's at least capable of acknowledging this or don't and acknowledge that it is not and cannot be foundational. While I don't really care about which choice is made (that has more to do with community priorities than anything else) making no choice seems fundamentally contradictory to me. Treating types (or categories) as fundamental smells of confusing maps for territories. And complaints of undecidability sound to me like "it would be inconvenient if what you say is true, so I choose to disbelieve it", which is not a real criticism if the issue is one of truth rather than merely an issue of convenience.
To be honest, I'd never describe myself as a fan of PRL-like approaches, even when I wrote this post. I just thought it was a good fit for the task at hand. I don't think I have any fundamental insights to give you about type theory. I can at least point to a few papers I've read on realizability and interaction which you'll hopefully find relevant and stimulating; they were for me. Though nothing of their content is too relevant to my original post, which was just implementing a stray idea more than anything, and I'm not really interested in defending PRL in particular as I have no allegiance to it.
On the Computational Meaning of Axioms
Implicative algebras: a new foundation for realizability and forcing
Relational Type Theory
The work that got me interested in realizability in the first place wasn't even anything PRL related, it was actually Thomas Seiller's work on complexity-through-realizability. A lot of papers in that project are very niche and are harder to read, though, so I'm not sure what to reference other than these;
Why complexity theorists should care about philosophy
Towards a Complexity-through-Realisability Theory
