> Your argument here amounts to: if it's not descriptive, it must be prescriptive. By this argument, the entirety of pure mathematics is prescriptive. Is the id

> Your argument here amounts to: if it's not descriptive, it must be prescriptive. By this argument, the entirety of pure mathematics is prescriptive. Is the idea of a semiring a description of a particular natural object? But it makes little sense to claim the idea of semirings is normative. After all, math studies many structures that don't satisfy the semiring laws, as well! Yes, to some extent, mathematics is prescriptive. Publishing a paper on semirings or computable functions means that you think these objects are interesting and should be studied. But pure mathematicians usually stop here, they don't pretend their research has value because it related to the real world somehow. It's just supposed to be interesting on its own. On the other hand, type theorists push their theory with the expectation that it is useful for creating computer programs despite decades of contrary, if any, evidence. I wouldn't mind types studied the same way that, say, first order predicate logic is studied. The fact that most of the type theory researchers seem to hail from CS departments seems to suggest that types would simply fade into irrelevance however. I also see a difference in the extent that mainstream mathematics is prescriptive vs descriptive. Certainly you would agree that most mainstream maths, say number theory or differential topology, is much less definition-heavy than type theory is. And most definitions in pure maths have auxiliary character, they are only interesting in that they help clarify proofs. Sometimes it happens that definitions turn from auxiliary to interesting in their own right; this happens mostly when the same construction makes sense in multiple context. In type theory, on the other hand, definitions, and not of the auxiliary kind, make up most of the work. The proofs are usually mere bureaucracy, with definitions set up so that the facts the researcher wants to hold do so essentially by definition. Thus the definitions, i.e. the prescriptive part, is really the main contribution of type research. > But it's certainly not the case that all PL theory studies the lambda calculus. PL theory includes work on verification of imperative programs; on macro expanders; on compilation techniques; and on pure logic. Well, the linked document is called "PL theory", so I simply assumed that it would cover all of it to some depth and not just a particular subfield. May impression is that the "type" paradigm is the dominant one in PL research and I simply assumed the authors of the linked paper have the same impression given their selection of material. I certainly didn't mean to discredit the other fields you mentioned, I simply can't have an informed opinion about them.