Found this Donald Duck comic from 1972: “Byte Makes Right” (or: The Computer, or: Too Intelligent a Robot)

https://scrooge-mcduck.fandom.com/wiki/The_Computer

The opening line is:

“This Magic Brain is Scrooge’s new Superthink XL! Just slopping over with artificial intelligence, it should simplify office work pronto…”

Slopping over with AI! Coincidence or ahead of its time by over 50 years?!

Phenomenal reporting from ProPublica. Big takeaways:

• FedRAMP is too understaffed to be effective.
• Microsoft never answered serious questions about its cloud security architecture.
• Despite a damning report, Microsoft's government cloud product was approved anyway.

https://www.propublica.org/article/microsoft-cloud-fedramp-cybersecurity-government

@ilyasergey: "I formalised and proved the correctness of Move’s new borrow checker in Lean: 39,000 lines of mechanised metatheory, produced in under a month with the help of an AI coding assistant. This post tells the story of how it went and what it means for the future of PL research."

https://proofsandintuitions.net/2026/03/18/move-borrow-checker-lean/

There is no complete program you can write in CBPV that you couldn't have written in CBV.

The difference is in what you can *abstract over*. In CBV you can only abstract over the "value types" whereas CBPV gives you a new sort you can abstract over: computation types. So you can't write programs in CBPV you couldn't write in CBV but you can write *libraries* that have no direct analogue.

So the difference as a programming language only starts to appear when you start doing higher-order constructions like recursive types and quantified types. In my group we are exploring this space with our language Zydeco (https://github.com/zydeco-lang/zydeco). One of these new abstractions we have in CBPV+forall is relative monads which we study in our recent PACMPL/OOPSLA paper (https://dl.acm.org/doi/10.1145/3720434).

8th Workshop on Intuitionistic Modal Logic and Applications (IMLA)
24–25 July 2026, Lisbon, Portugal
Affiliated with the Federated Logic Conference (FLoC 26)
https://sonia-marin.github.io/imla26/

Constructive and intuitionistic modal logics, and their connections with type theory and computation, remain foundationally and practically significant in computer science, logic, and related areas. These include applications in type disciplines, meta-logics for computational phenomena, and explanatory frameworks in philosophical logic. The workshop aims to explore theoretical and methodological issues at the intersection of constructive proof theory and modal semantics, as well as practical questions about which modal connectives and rules best capture computational phenomena at appropriate levels of abstraction.

**Invited speakers**
- Brigitte Pientka (McGill University, Montreal, Canada)
- Ranald Clouston (ANU, Canberra, Australia)
- More to be confirmed.

**Submissions**
We invite abstracts for contributed talks of up to *2 pages* (excluding bibliography). They may describe published work, unpublished work, or work in progress. We especially encourage submissions from students and early-career researchers.

Abstracts should be submitted via the workshop’s submission page:
https://submissions.floc26.org/imla/

(ctd)

#Logic #ModalLogic #CallForAbstracts

Some news: the first summer school on Programming Languages, Logic, and Software Security, will be held August 10–14, 2026 in Aarhus, Denmark.

The summer school offers intensive courses by leading researchers covering foundational and applied topics at the intersection of programming languages, formal methods, and software security. It is aimed at PhD students and advanced B.Sc./M.Sc. students active in the areas of programming languages, logic, semantics, and software security.

Dates: August 10–14, 2026
Venue: Aarhus University, Aarhus, Denmark
Webpage: https://conferences.au.dk/pls

Courses and Speakers:

Bas Spitters: The Rocq proof assistant and Gen-AI Tools for Formalization of Mathematics
Lars Birkedal and Amin Timany: Higher-Order Concurrent Separation Logic
Daniel Gratzer: Introduction to Type theory
Aslan Askarov: Language-Based Security
Anders Møller: Program Analysis

I'm writing this in English.

Not because English is my first language—it isn't. I'm writing this in English because if I wrote it in Korean, the people I'm addressing would run it through an outdated translator, misread it, and respond to something I never said. The responsibility for that mistranslation would fall on me. It always does.

This is the thing Eugen Rochko's post misses, despite its good intentions.

@Gargron argues that LLMs are no substitute for human translators, and that people who think otherwise don't actually rely on translation. He's right about some of this. A machine-translated novel is not the same as one rendered by a skilled human translator. But the argument rests on a premise that only makes sense from a certain position: that translation is primarily about quality, about the aesthetic experience of reading literature in another language.

For many of us, translation is first about access.

The professional translation market doesn't scale to cover everything. It never has. What gets translated—and into which languages—follows the logic of cultural hegemony. Works from dominant Western languages flow outward, translated into everything. Works from East Asian languages trickle in, selectively, slowly, on someone else's schedule. The asymmetry isn't incidental; it's structural.

@Gargron notes, fairly, that machine translation existed decades before LLMs. But this is only half the story, and which half matters depends entirely on which languages you're talking about. European language pairs were reasonably serviceable with older tools. Korean–English, Japanese–English, Chinese–English? Genuinely usable translation for these pairs arrived with the LLM era. Treating “machine translation” as a monolithic technology with a uniform history erases the experience of everyone whose language sits far from the Indo-European center.

There's also something uncomfortable in the framing of the button-press thought experiment: “I would erase LLMs even if it took machine translation with it.” For someone whose language has always been peripheral, that button looks very different. It's not an abstract philosophical position; it's a statement about whose access to information is expendable.

I want to be clear: none of this is an argument that LLMs are good, or that the harms @Gargron describes aren't real. They are. But a critique of AI doesn't become more universal by ignoring whose languages have always been on the margins. If anything, a serious critique of AI's political economy should be more attentive to those asymmetries, not less.

The fact that I'm writing this in English, carefully, so it won't be misread—that's not incidental to my argument. That is my argument.

RE: https://cosocial.ca/@timbray/116200896936074766

> When the person opening the PR gets credit for shipping and the reviewer bears the consequences of reviewing a bad merge, you have a structural problem no tool can solve.

In a pool of bad AI takes and cringy jokes, this is something you really want to read and reflect on. The issue predates AI, but AI is going to make it so much worse, that a conflict is nearly inevitable.