We have a new, 7th (sic!) volume of Software Foundations: Security Foundations
https://softwarefoundations.cis.upenn.edu/secf-current/index.html

Topics include noninterference, security type systems, secure multi-execution, cryptographic constant time, and speculative load hardening. And that's not even all, as the volume is still in progress, and some new chapters are upcoming.

#free #book #verification

— Здравствуйте. Мы — Свидетели Игоговы.
— Может, Иеговы?
— Нет.

The annual VerifyThis competition is collecting verification problems for the next one until February 8. The competition itself is scheduled for 11 and 12 of April, collocated with ETAPS 2026.

Also take a look at the https://verifythis.github.io/ltc/ — a real-world scale challenge, currently aimed at verifying memcached.

Оказывается, "чашка" не является мерой объёма кофе... 😏

Thorsten Altenkirch jumped the hype train and launched a podcast named "about logic", presumably, about formal logic and type theory:

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

If you haven't been to Wikipedia recently, they're celebrating the 25th anniversary:
https://wikipedia25.org

ДМК Пресс перевели и готовят к выпуску легендарную Engineering a Compiler, 3rd Edition:

https://dmkpress.com/catalog/computer/programming/978-5-93700-428-4/

Учебник не нуждается в представлении ни для кого, кто вовлечён в тему разработки компиляторов, поэтому просто отмечу, что в нём весьма подробно рассматриваются все стадии компиляции:
— лексический разбор
— синтаксический разбор
— графовые и линейные промежуточные представления
— анализ имён
— анализ потока данных
— оптимизация (на разных уровнях, все базовые алгоритмы)
— выбор и планирование команд
— распределение регистров
— основы JIT компиляции и оптимизации (с использованием трассировки)

Достаточно деталей и нюансов чтобы заполнить 800 увесистых страниц. 😏

Как нам пояснил представитель ДМК, соображения сроков выпуска и рентабельности не позволили провести тщательную техническую редактуру, которой книга более чем заслуживает. Это можно понять, но придётся смириться как минимум с "анализом живучести" вместо общепринятого "анализа времени жизни" в качестве перевода "liveness analysis". Вероятно, и с другими "особенностями перевода".

Ну, спасибо, что не стали изобретать "творческое" название, и взяли очевидное, предложенное в компиляторном чате. 😁

Не понимаю ажиотажа вокруг стендапа и импровизации. То, что они называют "прожарка" мы в школе называли "перемена". И если ты был успешен, то в награду получал пиздюлей, а совсем не денег.

И вот эти люди в очереди к открытому микрофону — чем они в школе занимались? Пропустили всё самое интересно, и теперь пытаются наверстать?

Nobody really knows LaTeX, so OpenAI made their own Overleaf with GPT-5.2 that writes for you:

https://openai.com/prism/

AI-assisted proofreading, citations, and literature search

AI-assisted citations is a nice touch, we all well aware how nicely they work. 😏

In Soviet Russia Cognac isn't a kind of brandy, in Soviet Russia brandy is a sort of Cognac!

Относительно известная книжка Computer Science From Scratch в руках нашего любимого ДМК Пресс превратилась в

Python для профи: https://dmkpress.com/catalog/computer/programming/python/978-6-01140-652-9/

Видимо, разница в названиях отражает разницу в уровне целевой аудитории...

Как бы то ни было, на "профи" материал не тянет — по крайней мере так говорит мой непрофессиональный взгляд. Автор (Дэвид Копек, к которому у меня претензий нет) рассматривает довольно разнообразный набор тем — создание интерпретаторов языков программирования, эмуляторов аппаратных систем, алгоритмическую генерацию изображений и основы машинного обучения — но делает это самым простым и поверхностным образом.

У меня нет сомнений, что поверхностность рассмотрения и простота программной реализации примеров — целенаправленное решение автора. Во-первых, книга получилась очень компактной — менее 300 страниц вместе с приложением, т.е. её можно быстро прочитать и прорешать. В то же время по каждой из затронутых тем написаны талмуды под 1000 страниц, и больше, чем по одному — чтение не для слабых духом. Во-вторых, для её освоения не требуется особых предварительных знаний ни теоретического, ни инженерного толка. Ну и в-третьих, её не скучно читать, написано человечным языком без зауми.

По итогу, книгу можно рекомендовать студентам и начинающим разработчикам, которые хотят расширить профессиональный кругозор за пределы Веб-оперденей без заныривания на 50 метров в омут профессиональной литературы. Для этих целей — почти идеал. Напоминает мне про серию "Seven X in seven days", только ещё проще и ближе к мейнстриму.

Yeah, Edgar Wright knows his home work. Not only the Running Man of 1987, but also the Demolition Man. 😏

https://www.quantamagazine.org/how-we-came-to-know-earth-20250915/

Curious, but too fancy to read on a phone...

2026 can become a year of a new Nobel Prize in Climate

https://www.climatenobelprize.org/

OPLSS this year offers a pretty stellar lineup of lectures, including Simon Peyton Jones on Verse:

https://www.cs.uoregon.edu/research/summerschool/summer26/topics.php

https://dl.acm.org/doi/10.1145/3607832
"Special Delivery: Programming with Mailbox Types"
Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, Phil Trinder

A very neat peace of work. It ties up a pretty diverse and somewhat obscure research topics:
— Regular Expressions (over types, what you expected?)
— Subtyping
— Constraint Solving
— "Backwards" Bidirectional Type-Checking (synthesizing necessary contexts and constraints along the checking)
— Quasi-Linear Types
— Second-Class References

The result is a practical algorithmic type system for Actor-based languages, capable of catching not only type mismatch errors, but also protocol violations (wrong sequencing of messages) and deadlocks. All in the face of selective message receive. Darn impressive.

#plt #paper #actor #typesystem

Null hypothesis, motherfucker!!! Can you reject it?!

4th ECUMENICAL meeting will be hosted in Stockholm from 18 to 20 February 2026, with online only participation available.

https://sites.google.com/view/ecumenical-4th-meeting/

Registration form: https://forms.office.com/e/6e7iXXPFES

Logical ecumenism aims to provide a unified framework in which “rival” logics may peacefully coexist. The Leverhulme Trust ECUMENICAL project explores the fundamental aspects of reasoning via proof-theoretic semantics (Pt-S), where the meaning of logical statements is understood in terms of proofs rather than traditional truth-based models. The ECUMENICAL Pt-S approach seeks to provide a unified framework for different logics, serving as a common ground in which meaningful interactions may occur between them and enabling novel methodologies in the study of logic.

YT Music recommendations blow my mind. Impeccable logic and the deepest insight into my tastes.

https://www.youtube.com/watch?v=oFGc4hGJRJQ
Dan Ghica is talking about Huawei and their programming language Cangjie. Now.