https://rustfoundation.org/media/guest-post-rust-is-tier-1-language-at-microsoft/

Alright, the last remaining coolness points of Rust have ebbed away. Rust is now king of the hill, and the era of the second generation of systems languages is in full swing. So I think it's time to start imagining the third generation!

We have the terms computer scientists and computer engineers; why not add the terms computer logicians and computer mathematicians to the mix?

I do think that computer mathematicians and computer logicians are somewhat different from a computer scientist. For instance, @shriramk is a true computer scientist; he experimentally derives new empirical facts about computing. The type theory community has historically mostly consisted of computer logicians and computer scientists, but for instance HoTT, SOGATs, synthetic Tait computability, brings type theory into computer mathematics. Domain theory is of course an early instance of computer mathematics as well.

(I somewhat prejudicedly associate “computer logician” with tedious syntactical proofs and “computer mathematician” with semantic proofs.)

I particularly love this bit: I want to copy this slide for my next presentation: https://youtu.be/Nb_TQpwam54?t=538&is=V9IKgN-Cxaj85P18

I aim in my research to achieve the perfect blend of crackpottery and plausibility of actual progress found in the promotional materials for the Terpstra keyboard http://terpstrakeyboard.com/

I will not live in a pod, I will not eat the bugs, and I will not outsource my brain to the evil sand.

I'm getting good recommendations from this, but it's also sharpening my idea of what I want. Which is a journal that analyzes various parts of society and then gives policy recommendations from various schools of leftism. E.g. “in an anarcho-syndicalist regime, X aspect of the problem wouldn't exist because of worker ownership, but Y aspect would remain salient and in fact even more difficult.” “We know from (similar situation in USSR) what a Stalinist approach would be, and it succeeded/failed in this way.” I feel like this would do a good job of opening up the policy Overton window.

Basically, I want a journal that publishes a bunch of “three revolutionaries walk into a bar” jokes, but serious.

Do people have recommendations for socialist/anarchist journals/newspapers/online magazines to follow? I'd be especially interested in any that have long-form articles which are not just about current events.

Some thoughts on document formats. https://owenlynch.org/blog/hypertext-documents/

And then instead of 30 minute talks, each day starts with 4 lightning talks and then the rest of the day is reading the source code for the presented languages.

I want a PL conference where the only allowed submissions are new programming languages and the acceptance criteria is coolness.

Someone needs to start a grant program for algebraic geometry and call it the fellowship of the ring.

Am I so crazy to want a general purpose programming language with

1. Reasonable abstraction facilities
2. Reasonable performance
3. Reasonably short, conceptual proofs of correctness for all relevant system properties (normalization, denotational semantics, etc.)

???

I think that this is in reach with the technology of SOGATs and Logical Relations as Types, and this is what I'm trying to do with Hippogriff.

The responses to this prove that humans rock :)

I'm trying to stick to my "ask mastodon rather than chatgpt" habit: does anyone have recommendations for interesting places to visit in Paris?

Cracking myself up over my morning oatmeal imagining if the proof assistant currently known as Rocq had instead been renamed "Le Chicken".

You can find slides for the TYPES2026 talk I just gave on my website: https://owenlynch.org/archive/2026-types/1.html.

These slides include hippogriff (https://tangled.org/owenlynch.tngl.sh/hippogriff/) compiled to WASM, so you can edit the code snippets and run them with ctrl-enter to see what happens.

Just picked up from "Logical Relations as Types" the practice of not saying the words "beta rule" and "eta rule" and instead saying "computation rule" and "uniqueness rule".

I feel like I would have been much happier if people had used this terminology when I originally learned type theory, and I'm definitely going to use it next time I teach someone.

While I'm on that subject... I like thinking about the four rules as answers to the four questions.

How can I make an element of this type?
How can I use an element of this type?
What happens when I use an element of this type?
Are there any other sneaky elements of this type? (No!)

Authors should be in a deterministic order irrelevant to contribution status, but alphabetical means that people with last names that start with A always get to be first.

Proposal: order by hash, using the year of publication as a salt.

I just learned that there was a brief point in time where people referred to "typescripts" (drafts which had been *typed* rather than handwritten), until I suppose everyone typed everything, so it would no longer be confusing to have a non-handwritten manuscript! Funny bit of English on a Sunday for you all!

I'm implementing a type theory where the top-level bindings are *judgments* in the theory, rather than closed forms (this is important because I only have a restricted pi type). This means that evaluating an identifier (in the context of nbe) doesn't necessarily produce a "value" in the traditional sense. So I have two options:

1. Have eval return a sum type of (closed value, judgment)
2. Extend my type of values to include these "non-values".

Has anyone else run into this kind of problem before? Do people have recommendations for solutions?