I am saddened to report (from today's print version of Le Monde) the passing away of the great French computer scientist Jean-Raymond Abrial. He is a pioneer in formal methods and their applications, particularly through three major innovations:

- The "Data Semantics" model.

- The two successive versions of the Z specification language.

- The remarkable B method and tools. One of the most spectacular achievements of practical formal methods was the groundbreaking verification of the security system of the Paris Metro's "Line 14".

A major loss for computer science.

Bertrand Meyer

😢

https://uu.varbi.com/en/what:job/jobID:832747/

A PhD position at Uppsala University (Sweden) on the topic of "Parametric Floating-Point Reasoning".

Floating-Points are still hard, but it's nice to know somebody works on their verification. 😁

Если кто-то интересуется, то сообщаю, что Replit охуели:
https://replit.com/pricing

Теперь на бесплатном плане можно создать только 10 "приложений". Вообще, в принципе. Не задеплоить и запустить, а создать.

https://www.youtube.com/watch?v=X3EVWeh21jA

WOW! That's something.

https://scp-wiki.wikidot.com/scp-6001

Surprisingly good and unexpectedly heartfelt. Though, maybe, it's just the right moment for me...

https://europroofnet.github.io/Kutaisi25/
School on Symbolic and Statistical Methods for Reasoning and Processing Formal Expressions
Kutaisi, Georgia
July 7th-11th 2025

Damn, I bet the registration is closed. And it's too late to adjust my schedule for it...

https://www.lms.ac.uk/events/lectures/hardy-lectureship#Hardy%20Current

Emily Riehl is having a tour across the UK! ∞-Category greatest hits! 😁

Ещё одна книжка от ДМК про #causalinference
https://dmkpress.com/catalog/computer/data/978-5-93700-365-2/
"Причинно-следственный анализ в науке о данных"

Несмотря на #datascience в названии, в большей степени является введением в Causal Machine Learning (#CausalML) в целом и DoubleML в частности. Что? вообще-то? хорошо и интересно.

В любом случае, автор делает акцент на вопросах практического применения статистического вывода причин и эффектов, в каких случаях он подходит, а в каких — нет, и что делать чтобы подходил хорошо и давал осмысленные (и обоснованные) результаты. В частности, подробно обсуждается A/B тестирование.

Для этого в книге даётся много примеров кода на R и Python.

Одновременно с этим рассматриваются более "классические" методы, такие как инструментальные переменные, difference-in-differences, propensity scores и causal graphs a-la Judea Pearl (вместе с понятием d-separation).

Автор не чурается математики, и в приложениях приводит доказательства ряда "технических" статистических теорем о свойствах рассматриваемых методов.

Некоторые сомнения вызывает вопрос перевода технических и статистических терминов, как и корректность словосочетания "краткое главление". Но есть надежда, что ещё успеют исправить хотя бы опечатки.

Раз уж начал обозревать анонсы от ДМК...

https://dmkpress.com/catalog/computer/statistics/978-6-01140-653-6/
"R за пределами статистики", которая на самом деле "R без статистики".

Ещё точнее было бы назвать её "R для не-программистов". Тогда для кого? Для почти нормальных людей — тех, кто занимается работой с данными с целью построения графиков, отчётов и презентаций.

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

Так что если вы читаете этот пост, то вам это всё не актуально, но у вас могут найтись знакомые, которым пригодится...

https://www.youtube.com/watch?v=KD18ddeFuyM

Edgar Wright directed a new "Running Man" movie based on the same Stephen King's novel. Bigger scope, more crazy characters, brighter colors and even more action.

Well, I don't think I saw a bad Edgar Wright movie yet... 😏

https://www.youtube.com/watch?v=HJBnlZKgeUg

What? No, WHAT?!

— Мы расширяем наш мракетинговый отдел.
— Может, маркетинговый?
— Нет.

https://verynormal.io

An Obsidian KB on #statistics in general and biostatistics specifically.

Sadly, https://en.wikipedia.org/wiki/Michael_Madsen passed away yesterday July 3, (reportedly) from cardiac arrest at the age of 67. RIP. 😞

Парадокс кошки.

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

Mario Carneiro is (slowly) proving the Lean 4 (kernel) correct in the Lean 4 itself:
https://www.youtube.com/watch?v=hAj81bYngDA

There are curious insights into Lean 4 metatheory and actual implementation.

https://www.youtube.com/shorts/cZB_OD5qCHo

A gentleman walking (and swimming) across most of the world, save for Antarctica, Australia and Africa. Still a lot of ground (and quite a bit of water and ice) to cover. 🤯

https://blog.sshh.io/p/how-to-backdoor-large-language-models

Turns out fine-tuning a LLM to secretly insert backdoors is pretty cheap and easy. Another twist on trusting trust. Don't trust LLMs you didn't train yourself. Like you don't use compilers provided be a third-party. 😏

https://www.minimax.io/news/minimaxm1

Another Open-Source Open Weights (456B) LLM, this time from Singapore.

Other twists include
— 1 million input tokens and 80k output tokens (that's a lot)
— a new reinforcement learning algorithm: CISPO
— a hybrid-attention mechanism incorporating Lightning Attention

Benchmarks look pretty impressive. 😁

Книжку Григория Сапунова про JAX переводят на русский язык:
https://dmkpress.com/catalog/computer/data/978-5-93700-192-4/

Оригинал издан Manning:
https://www.manning.com/books/deep-learning-with-jax

Сапунов теперь, видимо, больше всего знаменит своим каналом @gonzo_ML — что полностью заслужено, канал отличный: интересный и познавательный. В прошлом, видимо, был знаменит своей работой в Яндекс.

JAX знаменит своим JIT, Automatic Differentiation и поддержкой Google TPU. И там ещё всякого разного вокруг накрутили.

В общем, интересная штука.