https://plr.csail.mit.edu/

Apparently, MIT runs an annual seminar where they discuss with authors some old and new programming-related papers. This year's selection covers a broad range of topics from (black-box) testing of shader compilers' back-ends to empirical study of «prompt engineering»; from a decade-old paper on database query optimization to optimizing Datalog for GPGPUs to compiling sequent calculus; from program synthesis to an interactive debugger for Rust traits.

The seminar is open for virtual attendees too on Friday May 8th, 2026.

https://elixir-lang.org/blog/2026/01/09/type-inference-of-all-and-next-15/

For about five years Elixir contributors have been working on integrating a type system into the language and tooling. Starting with the development of a pretty novel and unorthodox type system.

I'm fascinated by several things:

— they still haven't dropped the project. Despite slow progress and obstacles in performance and usability they systematically overcome.

— they are deeply committed to the soundness of their gradual type system, which is tricky (and to my eyes they sometimes confuse soundness and completeness in the blogs at least)

— they put end-user (developer) usability front and center, in terms of speed and responsiveness, type inference to reduce annotation burden, meaningful error messages, etc.

Towards that goals the post references their work on
https://elixir-lang.org/blog/2023/09/20/strong-arrows-gradual-typing/
and the development of
https://elixir-lang.org/blog/2025/12/02/lazier-bdds-for-set-theoretic-types/
which are cool in their own right.

https://www.pathsensitive.com/2022/03/abstraction-not-what-you-think-it-is.html

Abstractions are not what they seem. Just like owls.

Cool post. It mentions λ-calculus, antiunification (and Gordon Plotkin), abstract interpretation, and even contains a primer on the fundamental theorem of homomorphisms from Gerry Sussman himself.

I'd only like to add that we can represent abstractions themselves in (some) programming languages, as long as we can reify abstract domains and abstraction mappings in the form of language constructs. Different constructs in different instances, but Type Classes indeed show up rather often.

BREAKING NEWS!

Lawrence C. Paulson of the Isabelle/HOL fame now also has a YouTube channel:

https://www.youtube.com/@lawrpaulson

Another piece of a bit stale news:

As of January 1, 2026, ACM completed its transition to full open access: all ACM-published articles and related research artifacts in the DL are freely available worldwide without barriers to reading or reuse.

https://www.acm.org/about-acm/acm-pres-on-oa-transition-and-dl-changes

This ain't no small change!

Забавно получается когда продумываешь какой-то текст в голове — с чего начать, чем закончить, как переходить от одного тезиса к следующему, — но садишься его набрать, и мысль идёт совсем по другой траектории...

For some reason they say "AI makes programmers obsolete, because anybody can make an app now", but nobody says "AI will push Shopify out of business because anyone can make a Web store now". Curious, huh?

https://dmkpress.com/catalog/computer/games/978-5-93700-437-6/
«Godot 4. Разработка игр»

Не компиляторами едиными! Я понимаю, что эта фраза не имеет смысла для «настоящих компиляторщиков», поскольку компиляторы закрывают для них все потребности: «развлечения», «mental challenge» (ЕВПОЧЯ) и т.д. Но тем не менее. 😊

Не так давно ДМК перевели книжку про разработку игр на движке Godot, и это весьма вовремя. Поскольку ещё менее давно в ранний доступ на Steam вышла игра «Road to Vostok». Которая уже стала «poster child» для Godot благодаря масштабу, сложности и качеству проработки как внутренних механик — физики, симуляции, — так и «внешних проявлений» — графики, эффектов, анимаций, звуков, и т.д.

Само собой, этой книги будет недостаточно, чтобы создать проект уровня «Road to Vostok», но она покрывает полный цикл создания 5 игр попроще: три 2D и две 3D игры возрастающей сложности. Что является главным достоинством руководства: автор не забывает про такие «мелочи» как меню игры и GUI, оформление уровней и переходов между ними, условия и экраны победы/поражения и т.п.

Среди других тем рассматриваются, помимо ожидаемых обработки ввода, анимаций, физики, — работа с 2D тайлами, использование частиц в 2D и 3D, основы процедурной генерации и подгрузки уровня «на лету» и звуковое сопровождение. Кратко описывается использование Git, других скриптовых языков помимо GDScript, интеграция с Blender.

На мой взгляд, слишком поверхностно охватываются математические основы графики — вектора, кватернионы, матрицы и прочая прикладная линейная алгебра — и создание материалов и шейдеров. С другой стороны, по этим темам написаны отдельные книги, и в одну невозможно засунуть всю существующую информацию.

Так что, если вы или ваши знакомые не имеют представления как сделать относительно простую игру при помощи Godot, но страстно хотят — эта книжка придётся очень кстати.

https://davidbessis.substack.com/p/the-fall-of-the-theorem-economy

A surprisingly long, but equally surprisingly deep and engaging post. Or I simply got used to shitty writing on the Internet, even before the advent of the GenAI.

I can see it turning out prophetic in a couple years. It's a kinda race between universities and grant agencies on one side, and Math AI startups on the other. And we all know how fast are the universities.

Well, VCs wanted to "disrupt" higher ed for ages, and now we have a good chance to see how far humanity can go without it.

https://antimonit.github.io/2024/08/15/compiler-design.html

Another short high-level overview of a compiler organisation, this one based on the Kotlin compiler for a change. It separately considers a Parse Tree, Concrete Syntax Tree, and Abstract Syntax Tree and provides nice diagrams. Also gives many references to actual implementations and some tools like ANTLR.

Интересно, ёмкость этих синих пластиковых мобильных туалетов на массовых мероприятиях измеряют в человеко-часах?

https://www.youtube.com/watch?v=iw9AiEG-Qww

I love scientific simulations so much! The perspectives are so epic, we might not survive the drama.

A guy working in an AI company once told me, if AGI is going to end the humanity, they want a front seat. Now I suspect they're in a wrong seat. Probably in a wrong theater entirely.

News about future event for a change:
https://tech.cornell.edu/arxiv/

arXiv goes corporate independent (of Cornell) non-profit on July 1st.

Well, if they at least make a donation process simpler, that alone will be a big win. Last time I tried it was ridiculously hard to give money to arXiv — thanks to Cornell, or US regulations, I guess.

By the way, they're currently looking for the first CEO, an exciting opportunity, ain't it? 😁

Also, turns out arXiv is around for the last 35 years, basically, whole of my life. I'd never guess...

Я не понял — он кого злоумышленником назвал??? 😡

https://www.kickstarter.com/projects/altavisionfilm/scp-red-window

Stephen Hancock of the «SCP: Overlord», «SCP: Dollhouse», «STALKER: Shadow of the Zone» and a couple more short movies fame has launched another Kickstarter for a SCP short horror video.

The guy is no joke and delivers very high-quality professionally crafted films. I'm pretty hyped.

https://www.youtube.com/watch?v=9ab8AS1M-o4

Lean 4 comes closer and closer to Isabelle/HOL! 🤣

Jokes aside, that's incredibly interesting research direction. In a nutshell, they combine backward and forward proof search, employing "traditional" search-based methods for the former and a fine-tuned LLM for the latter. Pretty clever, sorta "best of both worlds".

The downside is the LLM is still in the middle of the fine-tuning process, so we might not see a release for another half-year.

Also, the typewriter UI and interface is curious in itself. Could be a fun and meaningful interaction mode for a proof assistant. Reminds me of Isabelle/HOL again. 😁

Камамбер и Кукумбер — братья, что ли? И сестра их — Кукушка?

https://songlh.github.io/paper/go-study.pdf
„Understanding Real-World Concurrency Bugs in Go“

A 2019 empirical software engineering paper giving an overview of several categories of concurrency bugs in some of the well-known Go projects like Docker, K8s, etcd, etc.

Funny enough, broadly speaking, developers are better at using old shared-memory synchronization primitives like Mutex, than message-passing synchronization through channels, especially in the presence of shared state.

The Beneficial AI Foundation and the Lean FRO launched a public open-source project to specify and verify the implementation of the Signal messenger crypto libraries and protocols:

https://www.beneficialaifoundation.org/signal-shot

https://www.beneficialaifoundation.org/blog/signal-shot