The Eternal Doorman

See ICFP 2026 .  Isidore Mohr - Girard's Paradox as Structure Music. See Demo: Girard’s Paradox as Structure Music by Isidore Mohr. I present a translation of Girard's paradox into music using Soundproof, an in-progress system for translating proof terms of dependently typed lambda calculus into electronic music according to their tree structure. I explore methods of representing tree structures sonically, and points of choice in the translation and presentation of the result.   You can listen to the whole album at  https://isdra.bandcamp.com/album/girards-paradox . Claire Wang on what the FARM thing is about ( 1:23:10 ) See CompositionCodes YouTube . Chen Xu - Drawing Algorithms as Modular Objects (starts at 6:08:53 ) This is really clever. You can abstract structure from random binary matrices by constructing finite automata to recognise certain regular patterns as they appear. Then as you progressively scan the matrix a network of automata appear and disappear ac...

See https://www.ninadavies.net/info https://www.ninadavies.net/bionic-step and Image Syncers at Axioma . This was recorded in February 2026. I hope she's OK! Subscribe to Aksioma . If that freaked you out, here's a video about friendly robots:  Subscribe to Asianometry .

See the paper at https://arxiv.org/abs/2602.19868 :   See Patrick Cousot & Radhia Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2--3):103--179, 1992 , and also Coinductive big-step operational semantics by Xavier Leroy and Hervé Grall and Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment by David M. Kahn, Jan Hoffmann and Runming Li.   Starts at around 3 hours .  See also  Patrick Bahr - Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations .  Subscribe to ACM SIGPLAN .

He left the ML part of the conference and today he's in the scheme bit, ... See Matthew Flatt on Rhombus and Syntax Transformers .  It's the first talk but YouTube's stupid interface won't let me see the time since the start of the stream until it's over, it only shows relative times from the end of the stream and so all I can tell you is that's around -1:56:43 when the stream start is at about -2:56:04 so maybe around 1:00:00 ? It's interesting to compare this with S. W. P. Steen's definition of a formal system he wrote in 1971. He went to great lengths to define the notion of a symbol, even including explicit metalanguage syntax for concatenation in generated symbols (because he needed to use x, x', x'', x''', ... for fresh variables) then defining type symbols Church-style using a structural induction over concatenated sequences. But for some reason he didn't feel the need to talk about subscripting symbols with type...

This is one of the first times I've heard a talk about this that actually seems to make some sense! Starts around 20:00 . 42:54 See Baker's paper NREVERSAL of Fortune - The Thermodynamics of Garbage Collection . Also  Theseus : A High Level Language for Reversible Computing  by Roshan P. James. See Free Quantum Computing by Jacques Carette, Chris Heunen, Robin Kaarsgaard, Neil J. Ross and Amr Sabry,  A computational interpretation of compact closed categories: reversible programming with negative and fractional types  by Chao-Hong Chen and Amr Sabry and Compositional Reversible Computation by Jacques Carette, Chris Heunen, Robin Kaarsgaard and Amr Sabry. 1:08:00 On the reversibility thing, it's weird, isn't it? See the bit starting at at page 18 of  EWD12345 . Nobody ever said anything to me about that. I guess it's a bit weird, but I don't care. I really enjoyed writing it, even though I was quite literally starving at the time. 1:16:42  On measuremen...

Starts at  2:20:06 . See  con-cat An experimental functional concatenative programming language inspired by Joy  and  Joy: Forth’s Functional Cousin by Manfred von Thun .  See also: On Krohn-Rhodes Theory for Semiautomata by Karl-Heinz Zimmermann. Representation Independent Decompositions of Computation by Attila Egri-Nagy and Chrystopher L. Nehaniv.  The algebras of graph rewriting by Nicolas Behr, Vincent Danos, Ilias Garnier and Tobias Heindel. See also  Two Great Talks on Programming Languages .  Subscribe to ACM SIGPLAN . 

If you pay YouTube for advertising you should seriously consider a class-action law suit. The way it works is that in the YouTube mobile app they put one of their standard controls "V" under an ad-click link in the top-left corner, so when people don't want your ad and don't want to continue watching the video they get sent to your ad and you pay for the click. The only way for users to get back to the screen they came from is to either wait for the ad to finish, then click the "V" or click the "back" button.  In case they say it's not the meaning of "V" to minimise the player, it is: It's there all through the video, any time you touch the screen. YouTube are just a bunch of crooks.

See  Basics of Personal Information Management: Finding the best tool(s)  and  https://karl-voit.at/ . It's also on GooTube and my comment there was: "I am enlightened and also a bit dismayed to hear how badly I have been doing this whole computer-using thing! 😂"  We could do so much better than the crappy pile of garbage we have right now! See  The T.H.E. Mutiprogramming System Console Message Interpreter  and  Edger W. Dijkstra's 1972 Turing Award Lecture . 

Programming languages as vehicles for thought. See  Matthew Flatt on Rhombus and Syntax Transformers  and  The T.H.E. Mutiprogramming System Console Message Interpreter .  Some parts are missing. See the transcript  EWD 340 . 5:42​ "The overwhelming problem was to get and keep the machine in working order. The preoccupation with the physical aspects of automatic computing is still reflected in the names of the older scientific societies in the field, such as the Association for Computing Machinery or the British Computer Society, names in which explicit reference is made to the physical equipment. What about the poor programmer? " 25:46​ "vastly different from what it has been up till now, so different that we had better prepare ourselves for the shock. Let me sketch for you one of the possible futures. At first sight, this vision of programming in perhaps already the near future may strike you as utterly fantastic. Let me therefore also add the considerations t...

Starts around 33 minutes in. Audio is awful for the first few minutes. I'm not sure whether this is really about Rhombus or Racket, ... It's mostly about syntax languages, but here they're even more than syntax languages because they act at the lexical level as well. They even have a notion of lexical scope. I guess it's the original notion of lexical scope! See The Syntax Model in Racket and  Binding as Sets of Scopes . Subscribe to ACM SIGPLAN .

This is really interesting. Talk starts at 18:05 or so. See Efficient strong functional programming with effects and compiler guided reference counting  and https://github.com/microsoft/mimalloc . When I tried to look up these projects this morning I got this: Subscribe to ACM SIGPLAN . 

This is an amazing phenomenon. This language kind of invents type systems as it goes,... It's a bit like what set theorists do, in fact. More on that later,... The talk starts around 34:50 . See  The Verse Calculus: a core calculus for functional logic programming . Also Simon Peyton-Jones' lectures at OPLSS 2026:  Types, Proofs, and Program Logics .  On denotational semantics see also Domain-Theoretic Semantics for Functional Logic Programming : 17:23 On models which are termination-insensitive. See  Two Great Talks on Programming Languages , in particular Shriram Krishnamurthi on the 1991 paper On the expressive power of programming languages by Matthias Felleisen. Subscribe to  ACM SIGPLAN . 

We don't have any decent operating systems unfortunately, but I keep thinking about this device, because it is a cool toy. I once programmed something like it in Microsoft Basic, of all things. All it did was allow the program to open new windows on the screen with widgets of various kinds which it could configure by calling procedures. So there was a widget which could display a list of items and the widget handled the scrolling as each item was added. There was another which allowed input strings and the widget made the data available as the return result of another procedure. There was a status bar widget which showed various flags according to procedure calls etc. etc.  But we have much fancier displays in the form of web pages, so it occurs to me that you could make a system like this allowing programs to interact with local web servers, one for each app. These could be multiple different processes each serving http requests on a different port. Then one of them would be the ...

See his Google scholar list of publications and  Narya documentation .  Some noteworthy papers: Homotopy type theory: the logic of space  (2017) Comparing material and structural set theories  (2019) Subscribe to  About Logic . 

I think that card-punch definition is actually the closest one. This was the first session today.  Her talk starts about 10 minutes in: The Q&A session was really good. See Lindsey Kuper - Interpreters Everywhere!   Subscribe to ACM SIGPLAN . 

Seems like there are lots of different shades of bisimilarity. Why didn't anybody tell me about compiler calculating? See Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations by Patrick Bahr. Talk starts about 2 hours into this livestream. Subscribe to ACM SIGPLAN .  

This is a really great talk. I hope Dana Scott gets to hear about this fixpoint model. Also the questions from the programming language semantics angle are very interesting. His answer is basically "Don't write programs like that!" See his book  Deterministic Concurrency . It's the first talk in this session. See ICFP 2026 . Before I listened to this talk I was thinking about what sort of a world it would be if we had tools where we could use synthetic mathematics to build languages (syntax and operational semantics) with certain abstract properties defined by Lawvere semantics. You would be able to compose different notions and factor out sublanguages which are well-behaved according to the functorial semantics. In this somewhere there is surely a kind of algebra of languages. For some reason though, people think it is better to develop separation logic and stuff to "reason" about any old garbage that somebody might try to write, and the people who make the...

See  ICFP 2026 Program . I just caught the end of an interesting talk by  Hongshuo Fan  who has been experimenting with musical gesture recognition. That would be interesting to try in collaborative composition projects too. Also Jared Gentner on what sounds to me like an interesting way to compose languages. It definitely works for performance programming! There was also a miniKanren thread. See  William Byrd on Relational Programming and Quines . Starts at 1:18:34 . At 3:08:42  Towards bottom-up enumeration in miniKanren via pruning and memoization. At  6:04:44 Compiling polymorphic relations without monomorphization.  6:52:18 Efficient Rational Unification for miniKanren.  Questions & Answers at 7:26:12 .  8:14:53 Lean, Mean miniKanren Machine.  9:03:12 Q&A. Subscribe to ACM SIGPLAN .  Also, tomorrow at 9AM Edward Lee on Deterministic Concurrency .  It is not uncommon, particularly in the early literature in co...

Somebody please inform the Vatican ,... See these articles: Phosphorus-nitrogen systematics of first-generation planetesimals constrain life-essential element delivery to Earth by Debjeet Pathak, Rajdeep Dasgupta and Naidhruv Iyer. Rain may have helped form the first cells, kick‑starting life as we know it by Aman Agrawal. The nature of the last universal common ancestor and its impact on the early Earth system by Edmund R. R. Moody et al . Intermediate stages in the origin of metabolism at a phosphorylating hydrothermal vent by Natalia Mrnjavac et al .  Also this on the origin of mineral gas!  See also this Patreon post by Anton and these articles:  Deep subsurface organic-rich shale supports abundant, diverse, and novel fungi  by Quinn S Moon et al. Rock-eating fungi flourish deep below our feet   (U. Michigan Press Office.)  Subscribe to Anton Petrov . 

See  CuriousMarc - Taking Apart an HP 16702 Logic Analyzer .  Some of this rings bells. I think I must have done an HP/UX upgrade from CD-ROM once,... Buy SCSI knives from  Jurassic Computing .  Subscribe to  Curious Marc . 

Born into the prominent political and banking Medici family of Florence, Giovanni was the second son of Lorenzo de' Medici, the de-facto ruler of the Florentine Republic, and was elevated to the cardinalate in 1489. Following the death of Pope Julius II, Giovanni was elected pope after securing the backing of the younger members of the College of Cardinals. See Pope Leo X  on Wikipedia. See also  Fugger family  (well in the sixteenth century they spelled words differently.)  Subscribe to  Uncover Things  (shit, etc.) and  Uncover History  (more shit than you can shake a stick at.)  Pope Leo XVI is going to make up for it I'm sure. Subscribe to Lena Petrova . 

This is interesting. See the paper  Hyperfunctions: Communicating Continuations  by Donnacha Oisín Kidney and Nicolas Wu. We use this framework to solve a long-standing problem: giving a fully-abstract continuation-based semantics for a  concurrent calculus, the Calculus of Communicating Systems. Finally, we use hyperfunctions to build a monadic Haskell library for efficient first-class coroutines. There' a POPL'26 talk on YouTube but they make you watch tons of ads. See also: Categories of Processes Enriched in Final Coalgebras by Sava Krstić, John Launchbury & Duško Pavlović. Faster coroutine pipelines by Michael Spivey. Continuations and transducer composition  by Olin Shivers and Matthew Might. Subscribe to ACM SIGPLAN . 

Both of  these talks are relevant to this post of mine:  The Story of Unix - Chapter Ω: The Captains All Jumped Ship . Douglas Creager on Concatenative Programming and Stack-based Languages  See  The Theory of Concatenative Combinators  by Brent Kirby.  Subscribe to Strange Loop .  Shriram Krishnamurthi on the 1991 paper  On the expressive power of programming languages  by Matthias Felleisen. He does a great job describing a quite subtle idea to a non-mathematical audience.  35:36 I really need to read this paper to understand exactly what is the difference between Ω and halt . [ 40:13 halt   is just call/cc ].  Subscribe to Papers We Love . 

There used to be this philosophy, that some people called an Operating System, ... The people who came up with the idea weren't so besotted with it as those who followed and they set out to do it better. That was called Plan-9 from Bell Labs . Ever since the Unix ship has just been sailing around, who knows where? Don't ask any of the crew. And Plan-9 ? Unix came with a new programming language and a new way to write programs, by composing them together using shell scripts. Plan-9 didn't . The Viewpoints Research Institute STEPS project was the sort of thing Plan-9 needed, but Viewpoints was terminated in 2018.  See Condensing Programs for more on functional components. See also these parts of the STEPS project: KScript and KSWorld: A Time-Aware and Mostly Declarative Language and Interactive GUI Framework by Yoshiki Ohshima, Aran Lunzer, Bert Freudenberg and Ted Kaehler and Open, extensible composition models (extended abstract) by Ian Piumarta. Douglas Hofstadter gave...

These things ran HP/UX : 7:05 Lamenting the software issues. It's because we never figured out how to write programs. People were too busy building fancy hardware to run garbage code. Eventually they gave up and now they build fancy hardware to run garbage LLMs that generate shit-loads of garbage code. It's good for business! [See Robot Languages and Robot Languages - Another Part ]. Part 2: Applying HP sauce to the PS/2 Model 77: Part 3:  Part 4: See https://github.com/schlae/snark-barker-mca   The full series of videos on this is here .  Subscribe to CuriousMarc . IBM's Micro Channel was their last-ditch attempt to regain a monopoly on PCs ( 30:43 ):  There was also the RS/6000 though: Subscribe to Asianometry .

My comment : This sounds a bit crazy to me. Why do you want distributed computing to depend on particular endpoints? I don't want my messages to be delivered to some particular machine, I want them to be delivered to me. So why do I have to maintain particular machines to receive messages? And the same goes for companies that are accepting orders from customers etc. etc. It just seems like people are stuck in a rut thinking about programming as something you do to make a machine do some particular thing, but it doesn't have to be like that. [Aha, that's what this bit is about: 45:55 .] Subscribe to ACM SIGPLAN .  See also  Ian McKellar on Fuchsia .

It  turned out the whole theory of Fourier Series is one particular instance of a general theorem about Representations of Compact Groups. See Peter-Weyl Theorem  and Pontryagin duality . See also  Dual Spaces, Lie Groups and Conservation Laws .  Subscribe to Daniel Tubbenhauer .  Sam Ritchie on a computer algebra system https://emmy.mentat.org/ inspired by Functional Differential Geometry by Gerald Jay Sussman and Jack Wisdom.  Subscribe to Strange Loop . Owen Lynch with some ideas on how to do computer algebra that get at this idea of generic operations that Gerald Sussman likes so much, and I think they are also why he doesn't have much time for statically typed languages. In a sense types are least fixed points and generic operations and general algebras are greatest fixed points. See How Could One Unify CMU and MIT  and David Jaz Maiers - Compositionality via 2-algebra . See his blog post  Algebraic geometry for the working progra...

This was from ADC2024 but only posted on YouTube in August last year: Somebody made a whole operating system and a GUI for Pipewire: https://github.com/dimtpap/coppwr . See  Using Pipewire to Make A Music Synthesizer  and the greatly expanded examples https://docs.pipewire.org/examples.html . A talk at FOSDEM in 2025 by Wim Taymans: PipeWire state of the union .  I came here after seeing a bit of Ian McKellar on Fuchsia  and Chris Ford on Birdsong . Subscribe to ADC . 

He has some interesting remarks to make about birdsong as culture. For example that the birds need to hear other birds in order to learn how to sing.  Subscribe to Strange Loop . Hunter Adams on a birdsong synthesizer and Jack Chaney and Arielle Huang on a tuning system with spectrum analyser: See their project web site: https://ece4760.github.io/Projects/Fall2025/aph74_jbc282/index.html . Subscribe to V. Hunter Adams .  Also, the Cornell Merlin project has a neural network for birdsong recognition that you can use on a Raspberry pi to recognise birds in the field: See this Hackaday post  Track Bird Visitors With A Raspberry Pi And A USB Mic . Subscribe to Teddy Warner . Back at Cornell, Ann Xu, Amy Wang, and Minjung Kwon made a fiendishly complicated spatial audio murder mystery game on a Rasperry Pi Pico: See the project page here .  Subscribe to V. Hunter Adams .

Aspects of this sound weirdly familiar , ... See https://fuchsia.dev/fuchsia-src/concepts/software_model . I was in a jail in Louisiana watching awful Halloween movies while this conference was going on. Subscribe to Strange Loop .

Subscribe to  Dustups . My comment : I was just looking at Shaun's latest video today and you can see he has so much land upstream that he can't break the flow before it gets into a wash then it's unstoppable. He needs a dozen people doing what Brandon does to stop the sheet flow before it gets into the wash. Subscribe to Grow Tree Organics . Brad's books in English and in Spanish: https://www.harvestingrainwater.com/shop/ . Subscribe to Brad Lancaster . 

She's also starting up her creative writing coaching again: Subscribe to Curious Wandering Souls .

It's what big tech might have been,...   Give or take an infinity of REPLs. See  Nada Amin - Metacircular Interpretation ad infinitum .  Subscribe to Laurie Wired . Subscribe to Kalman Reti .  There's some of the fraught MIT origin story of this company in the Epilogue to Steven Levy's book Hackers . See  How to Write An Emulator .  42:24 A 1988 Apple Macintosh that sold for $15,000, ...  44:30 See transcript at:  AI: Expert Systems Pioneer Meeting Session 1: Purpose, Structure, and Introductions and  CHM Releases New Recordings and Personal Stories with AI Expert Systems Pioneers.   Subscribe to Asianometry .

See  Amy Sandoval Interview With John Chowning  and  Amy Sandoval on Why The Yamaha DX7 Synthesizer Was Such A Thing . This interview is very different to the one he did with Amy.  My comment : That story ( 7:26 ) about needing five minutes of computer time to create two seconds of audio makes me feel like a spoiled brat! 😂 [See also 1:03:59 ] See  Entire MIT ITS Emulation Running on a Raspberry Pi 5 . 23:17 What's next for computers and music? He's hopeful! There are people who do have imagination. See  Szymon Kaliski - "Programmable Ink" .  35:15 His early experiences with reverberant environments. 37:30  acoustically characterizing spaces. See  Chavín de Huántar Archaeological Acoustics project . 1:29:58 The Samson box . It's in Paris now and they want it back!  Transcript of the interview available at  https://www.computerhistory.org/collections/catalog/300000261/ . See also  https://ccrma.stanford.edu/ . Subscribe to C...

Subscribe to About Logic . 

There are some interesting statistics in here.  Her Lorem Ipsum video is really brilliant.  I didn't watch this for ages because I thought I knew what it was about. Shame on me! Her Patreon: https://patreon.com/rabbitholevideo . Subscribe to Rabbit Hole .

You could do something like this for any output language though, I mean HTML or whatever. So you could interactively explore infinite output  from streams or non-terminating reduction processes.  Subscribe to  ACM SIGPLAN . 

See Contextual Embeddings: Implementing Bound Variables through Instance Resolution by Samantha Frohlich, Jessica Foster, G. A. Kavvos and Meng Wang.  I don't know if this is really Jessica Foster , internal evidence suggests the speaker is Samantha Frohlich.  See  About Logic - Dependent Types .  Subscribe to  ACM SIGPLAN . 

They had to take the digging buckets off though, to get it to go that fast.  Subscribe to NYPost . 

Developing mechanized specifications for JavaScript, WebAssembly, and P4 . This is what I meant by Metaprogramming and it works. This project was funded by the Korean Government. I wish I could pay them my income tax.   See https://wasm-dsl.github.io/spectec/ and https://github.com/es-meta/esmeta . Jihyeok Park - Trusted JavaScript Language Environments with ESMeta. See https://github.com/es-meta/esmeta   Xiaohong Chen - Programming Languages Must Have Formal Semantics. Period. See https://kframework.org/ The panel discussion on Real-World Programming Languages The Rust guy goes on and on and on. Definitely too much 'real-world' there. The problem is a huge chunk of what some people call the real world is just what Edsger W. Dijkstra called "Getting lost in complexities of your own making" and a lot of the real world just isn't in the purview of programming language and operating system designers at all because it is completely and utterly beyond reach. I mean t...

My comment : So it's not actually a VPN in that case, is it? I'm not even sure you could call it a VN. It's just an ordinarily FUN. Subscribe to Defensive Podcasts . 

Well, if you're like me, ... Subscribe to Asianometry .

See https://reticulum.network/  and  Ian Clarke - Freenet Update . He has a company https://buildwithparallel.com . Subscribe to Data Slayer . I saw this talk at 38C3 on YouTube:  My comment : Poor guy. Nobody's listening to him so he gets no feedback. I think he's doing it wrong. The first few requirements (disaster areas and places with scant network resources) preclude connectivity within minutes. Sometimes some people find themselves in environments where their messages aren't received for years. Also, the ability to communicate with one specific person anonymously is questionable. What's that for? To enable terrorism? Stick to sending poison pen letters you made from cutting words out of newspapers. Austin is nearly connected to San Antonio, ...  Subscribe to FUTO .

See  Meta Are Hiring Intelligence Analysts .  Subscribe to Naomi Karavani . 

This idea about elaborating relations under constraints is really interesting. See  Thorsten Altenkirch on NaÏve Type Theory and An Interesting and Useful Duality  and  Condensing Programs .    See miniKanren, live and untagged: quine generation via relational interpreters (programming pearl) by William E. Byrd, Eric Holk and Daniel P. Friedman and  https://minikanren.org/  for more on Micro Kanren ( 21:00 ). See also  What is Formal Logic?  and  Nada Amin - Metacircular Interpretation ad infinitum . Subscribe to Strange Loop . See A small embedding of logic programming with a simple complete search  by Jason Hemann, Daniel P. Friedman, William E. Byrd and Matthew Might and  Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics by Brysen Pfingsten and Jason Hemann where they describe a web interface to  a semantic model which lets users interactively view the reduction steps. Here are some rela...