How to make make-making makers make makes you’ve made!

Multi-language programs are ubiquitous and language designers have long been designing programming languages to support interoperability. We’ve had platforms such as .NET, JVM, and COM that facilitate interoperability, and languages such as Scala, F#, SML.NET, and many more that treat it as a central design feature. In a 2007 paper, Matthews and Findler pointed out that most multi-language research was focused almost exclusively on how to implement interoperability efficiently and not on the quite subtle semantics of these features. They presented a multi-language semantics framework that gives language designers a methodology for taking two languages, adding interoperability boundaries between them, and giving an operational semantics to those boundaries. I’ll describe the mechanics of multi-language semantics, how they support reasoning about the behavior of mixed-language programs, and discuss the impact that this tool has had in the last 15 years […]

see: https://dl.acm.org/doi/10.1145/1190216.1190220

This talk is about how to change the status quo to make it easier to build multi-language software.  I’ll argue that language designers should equip their “core” language with extensions, dubbed linking types, that allow programmers to annotate how their components should interact with features missing from their core language.  Moreover, toolchain developers should devise compilers and linkers that prevent linking with external code that violates safety or security properties provided by the core language, unless the programmer uses linking-type annotations to request such linking.

A lot of really interesting ideas in here. Unfortunately got lost in the notation since there isn’t a recording. Lots of great links within!

Webinar Series ‘Science Training Sessions’, American Psychological Association, June 2026.

So, apparently, we’ve been measuring depression horribly wrong for decades. Yay…

Too many programming languages researchers dismiss concrete syntax as an afterthought […] This received view ignores a critical factor: the human at the computer. Concrete syntax defines the principal interface through which programmers interact with the vast majority of programming languages. Moreover, this interface is hardly decoupled from semantics; even trivial-seeming differences in keywords, sigils, and indentation can affect how programmers utilize and reason about language behavior. Using examples from asynchronous control flow, gradual subtyping, first-class functions, and more, I will make a case for the importance of concrete syntax, why language designers often overlook it, and what this implies for those of us who care about the usability of abstractions. Finally, I will describe some preliminary work evaluating the role of lexical ambiguity in programmer comprehension of type system features.

A return to an old flame of mine.

see: https://slim.computer/concrete-syntax/

Very nice set of slides on a phenomenon I’ve been trying to put a name to. The discussion of discrete dynamical systems over the integers can be found in “arithmetic dynamics.”

see: https://en.wikipedia.org/wiki/Arithmetic_dynamics

see: https://en.wikipedia.org/wiki/Height_function

This thesis argues that digital services need not come at the cost of our privacy. As a step towards this goal, this thesis introduces cryptographic protocols and secure systems that let users fetch and search over public data, without revealing anything about what they are fetching or searching for. We first present SimplePIR, an encryption scheme that can perform linear computations on encrypted data at near-unencrypted speed. Building on SimplePIR, we design Tiptoe, the first cryptographically-private web search engine. Tiptoe allows a user to search over hundreds of millions of webpages in seconds, all while revealing nothing about its query to the search provider; its core private-search techniques have seen adoption in Apple’s iOS (“Enhanced Visual Search”). Finally, we describe new private-information-retrieval protocols that circumvent Tiptoe’s linear-time bottleneck and could let private-search systems scale larger yet.

Coding agents can now produce code faster than humans can review it. Techniques that minimize the amount of code that can affect system correctness are therefore a major goal in the field. The Axon project used a coding agent to build a complete verified compiler — source language, operational semantics, optimizations, machine model, and mechanically checked correctness proofs — in 34 days under one supervisor.

The talk discusses how the project combined four validation techniques — testing, credible compilation, formal verification, and code audits - to maximize development velocity while minimizing the amount of unverified/unchecked code.

We present the overall architecture of the compiler, the roles that the different validation techniques played in the development, results from the Axon implementation, and implications for other agent centric development efforts.

see: https://arxiv.org/abs/2605.01660

This talk will focus on one such verification approach that takes as input a design under verification (DUV), modest architect-friendly DUV metadata, and a HW-SW contract. The approach automatically generates many simple formal properties that provably compose to imply the contract, and then evaluates them against the DUV to assess contract compliance. The enabling insight is that many important HW-SW contracts decompose into instantiations of a small, finite set of property templates, fillable automatically from the supplied metadata or from the results of evaluating other generated properties. This verification approach eliminates manual property writing, targets full HW-SW contracts rather than coverage metrics, and yields properties simple enough that commercial formal model checkers can produce unbounded proofs for most, even on complex designs.

A bit rambly but it’s lighthearted fun. Christine talks about the way you can shape Lisp in a general way, and how Lisps sort of lack of a shape allows it to be shaped so well. Not really about macros despite that naturally being a component of this ability, but moreso the philosophical and fundamental design of uniformity that Lisp brings to the table.

A bit rambly but it’s lighthearted fun. Christine talks about the way you can shape Lisp in a general way, and how Lisps sort of lack of a shape allows it to be shaped so well. Not really about macros despite that naturally being a component of this ability, but moreso the philosophical and fundamental design of uniformity that Lisp brings to the table.

A nice walk from homotopy to Lie theory to category theory to combinatorics.

Can’t fully understand because there are no words, but the author looks to be making a very neat connection between coalgebras and the executions (here “traces”) of transition systems. Became aware of her work through Adjoint School 2026.

via: https://www.cs.uni-salzburg.at/~anas/talks.html

Scientists and engineers like to describe processes or systems made of smaller pieces using diagrams: flow charts, Petri nets, electrical circuit diagrams, signal-flow graphs, chemical reaction networks, Feynman diagrams and the like.   Many of these diagrams fit into a common framework: the mathematics of symmetric monoidal categories.  When we embrace this realization, we start seeing connections between seemingly different subjects.  We also get better tools for understanding open systems: systems that interact with their environment.  This takes us beyond the old scientific paradigm that emphasizes closed systems.

Going down the categorical systems theory rabbit hole; very good exposition from Baez as per usual. I also finally know what a monoidal category is, so that’s pretty handy. I ought to read the paper this talk is based on at some point.

see: https://math.ucr.edu/home/baez/rosetta/

via: https://en.wikipedia.org/wiki/Monoidal_category

Acsets are a novel infrastructure for handling data of different shapes, based on category theory and implemented in Catlab.jl. Acsets generalize both graphs and dataframes, and allow a much more general approach to data manipulation than was previously available. We will discuss both the mathematics of acsets and some of the metaprogramming techniques we used to implement them in Julia. Finally, we will give examples of how acsets have been key in developing many projects in AlgebraicJulia.

Probably the best AlgebraicJulia tutorial on the planet LOL.

Great pair of talks.

via: https://golem.ph.utexas.edu/category/2025/10/a_complex_qutrit_inside_an_oct.html

These are the videos from Derbycon 2018:http://www.irongeek.com/i.php?page=videos/derbycon8/mainlistPatreon:https://www.patreon.com/irongeek