Robert Widmann

Shame on you @microsoftteams.bsky.social for requiring scanning for devices on the local network. You do not need this capability, and the fact that you cripple your app and eject people from calls if they turn it off is idiotic. Say no to your marketing and product people for once.

since NYT games has revealed people like constraint solving, i figured i'd pitch them a struct packing game

it'll just cost them a copy of libclang - a measly half a gigabyte of text

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

RETVRN en.wikipedia.org/wiki/Enforce...

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

Webular Expressions by Cisco

YouTube video by Flesh Wound U.K. - The Only Thing She Needs

@adamneely.bsky.social Heard the opening to this and thought it might pique your interest as a lover of Making 4/4 Hard youtu.be/EGcqyN-TeDc

Free startup idea: Put a convincing Perplexus simulation into the Vision Pro app store and charge me $20 for it immediately

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

x.y@xy.com

always works

Grindr should acquire Niantic send skeet

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

That flaw: impredicatvity. Mind you, don’t think of that in the modern sense(s). He was searching for a way to characterize problematic formulae in a systematic way, but personally I don’t think he ever really found it. His idea being such things lead to “vicious circles” - in the modern sense.

Russell’s motivations for building the thing are very far removed from programming, you will recall. His goal of grinding paradoxes out of the foundations of mathematics was predicated on his belief that such paradoxes were the result of a singular flaw.

There’s no denying Russell as the originator, as he’s got the post-matter of Principia Mathematica as the source of the first attempt. Reading volume 1, you get your first intro to the thing and a definition, but no elaboration. Presumably volume II was meant to contain such a thing.

Poking back in time to the history of types, and am interested to discover it took Russell quite a few tries to get a system of types going, and the systems he stood up bear a resemblance to the modern interpretation of the concept.

A wiry-haired french professor stands in front of a power point presentation pointing at three dense bundles of knots

“Imagine this, if you will, as a program”