Posts

More FARM Projects

Image
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...
Post a Comment
Read more

Nina Davies - Synchronising With Images

Image
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 .
Post a Comment
Read more

David Knothe and Oliver Bringmann - Combining Big and Small-Step Semantics to Verify Loop Optimizations

Image
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 .
Post a Comment
Read more

Matthew Flatt on Rhombus and Racket

Image
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...
Post a Comment
Read more

Amr Sabry - What is "Quantum" about Quantum Computing?

Image
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...
Post a Comment
Read more

Attila Egri-Nagy on a Concatenative Logic Programming Language

Image
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  Two Great Talks on Programming Languages .  Subscribe to ACM SIGPLAN . 
Post a Comment
Read more

YouTube Click Fraud - Generating Fake Ad Clicks

Image
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.
Post a Comment
Read more

Karl Voit - Managing Your Personal Information

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 . 
Post a Comment
Read more

Edger W. Dijkstra's 1972 Turing Award Lecture

Image
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...
Post a Comment
Read more

Matthew Flatt on Rhombus and Syntax Transformers

Image
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 .
Post a Comment
Read more