I seem to recall (Knuth’s?) telling that as a result Boot ROM was called ‘initial orders’

Big fan of what Roslyn does here where you model the idea of busted code with missing and unexpected AST nodes. We stole this for SwiftSyntax and its parser. We recover by accumulating the garbage that sits between the current lexeme and the next valid lexeme and sweep it into an ‘unexpected’ node.

COBOL is a modern language

- Modular (you’ll be maintaining 5-20,000 programs at a time)
- Supports up to 8 physical switches and one bell (fuck you C++)
- Has robust TYPE system, including modern features like page layout handling and section grouping wait why are you weeping

Online email verification remains a lost technology for the average Jabbas Crypt mf, so

x.y@xy.com

always works

My hunch is it takes quite a while to actually get to that point, say the 1950s or so. You get “types are good for computers” with the combinatorialists having a go at it around that time, but not necessarily “types are good for data”

Exactly. It’s precisely that inflection point that I’m after. Up next is the real Ramified Theory of Types, then Ramsey and his Wittgensteinian approach to the thing, then Tarski.

My constructivist brain balks at this idea. 0 as a canonical term of type ℕ and a canonical term of type ℝ but denoting the same object feels deeply wrong to me. Of course Russell was not thinking of any of this when he wrote his definition down.

So to Russell, the answer for “what is a type” per his definition, is the collection of objects you can insert into a function φ and wind up with a meaningful output φx.

As for avoiding circles, he doesn’t _quite_ get to Tarski-style stratified constructions but he’s awfully close isn’t he? The whole idea of the types, after all, is that you can make sure you have an ever-shrinking set of quantifiers in formulae, a set theorist may dare to call it well-foundedness

He also makes a blunder by admitting typing for propositions at the same level as ordinary terms, which makes his system immediately unsound.

Now for the not so good, remember Russell is not a constructivist. A mathematical object is summoned to appear when named. A type merely binds that object to a classification. It is possible for an object, therefore, to be bound to many such classifications, so long as doing so creates no circles.

There’s a brilliant thing in here, and there’s a lot of not so brilliant things in here. Russell recognizes in his types that there are useful divisions to be had of mathematical objects, and that you can both properly restrict your inputs and outputs AND avoid vicious circles with proper structure

Anyhow, back to the types. Russell’s types are defined at the level of objects rather than metamathematically, a theme that pervades his work. “A type”, sez Russell, “is defined as the range of significance of some function” which he writes as φx

No, there’s something special about these problematic formulae, he says again, they have a kind of infinite (often “growth”) process in their meaning - as in the barber paradox - which leads to a revision by Russell to his structural rules: You can’t have a collection as a constituent of itself.

They argue with him about these schemes from the wrong direction, that there are useful formulae that quantify over the range of discussion yet do not necessarily lead to paradox. Consider

“the tallest among them”

A sentence quantifying over some people, naming one, but not problematically so.

His interlocutors are confused by these, to the point they even mistake him for a constructivist! “Of course”, they reason, “he isn’t comfortable with “impredicative” constructions”. To the constructivist, you cannot form such objects in your mind, to do so would violate temporality.

He spends a lot of paper arguing with Quine and Gödel about his different attempts to actually write down criteria, all fail. He tries
- Formulae that are “too big”
- Formulae that look like {some set of recursive definitions}
- Formulae that have quantifiers over the range inside them