Сюрприз! Откройте мир гонок!

Дружелюбное введение в многопоточное программирование.

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

"Two-Dimensional Kripke Semantics" by Alex Kavvos
November 13, Thursday

Proof Society Seminar, Monday 17.11.2025, 14:00 CET

Juliette Kennedy, University of Helsinki

How first order is first order logic?

Fundamental to the practice of logic is the dogma regarding the first order/second order logic distinction, namely that it is ironclad. Was it always so? The emergence of the set theoretic paradigm is an interesting test case. Early workers in foundations generally used higher order systems in the form of type theory; but then higher order systems were gradually abandoned in favour of first order set theory—a transition that was completed, more or less, by the 1930s.

In this talk I will look at first order logic from various points of view, arguing that the distinction between first order and higher order logics, such as second order logic, is somewhat context dependent. From the philosophical or foundational point of view this complicates the picture of first order logic as a canonical logic.

The seminar takes place via Zoom:
https://bham-ac-uk.zoom.us/j/84261727269
Meeting ID: 842 6172 7269

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

An interesting approach to teaching Programming Languages and Computer Science more broadly. Features some curious historical and contemporary references.

Волею судеб обнаружили себя в уездном городе Д., где ни один магазин не продаёт воланчики для бадминтона. При этом ракетки продаются с завидной настойчивостью, но воланчики не поставляются ни в комплекте, ни самостоятельно. Как предполагается играть в бадминтон без воланчиков — загадка. Вполне возможно, что никак, поскольку я действительно не встретил ни одной играющей пары...

After almost 8 years of development Unison 1.0 is finally released:
https://www.unison-lang.org/unison-1-0/

I don't see anything particularly new in the release, but for those who didn't follow, nowadays Unison "ecosystem" features a GUI IDE, a NPM-like library hosting, and a dedicated Cloud offering still.

BTW, it has been open source for a very long time:
https://github.com/unisonweb/unison

https://blog.jetbrains.com/ai/2025/11/why-diffusion-models-could-change-developer-workflows-in-2026/

Apparently, some Open-Source (and closed source too, of course) Text/Code Diffusion models are already here. I personally think they are much more prospective for programming than purely autoregressive models.

Unfortunately, at the moment Text Diffusion models perform mostly worse. Which is quite expected as long as they are much more recent invention, and don't yet enjoy years of engineering improvements.

Augmentin

On one hand, it's an ordinary antibiotic. On the other hand, if you're a cyborg with augmenting implants, antibiotics are very likely to be crucial for you due to constant infection concerns.

If you aren't subscribed, Stephen Hancock, one of the main creative forces behind SCP: Overlord, SCP: Dollhouse, and STALKER: Shadow of the Zone, released another excellent SCP short film two days ago:

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

Dear colleagues,

At AWS re:Invent 2025 in Las Vegas, we announced the AWS Nitro Isolation Engine [1, 2, 3], a formally verified enhancement to the AWS Nitro System that enforces isolation between virtual machines hosted on AWS's new Graviton5-based EC2 instances.

Nitro Isolation Engine represents a significant deployment of mechanized proof in production infrastructure, and we therefore wanted to bring this to the attention of the formal methods and programming languages communities. This work builds directly on decades of advances in interactive theorem proving, program verification, and programming languages theory, alongside landmark projects—such as, seL4 [4], CertiKOS [5], SeKVM [6], and many others—that were inspirations for this work.

What is Nitro Isolation Engine?
Nitro Isolation Engine is a small, trusted computing base written in Rust that sits beneath the AWS Nitro Hypervisor, providing a security isolation boundary between the hypervisor and guest virtual machines, and between co-tenanted guest virtual machines. The Nitro Isolation Engine controls the critical hardware features required for isolating customer workloads, primarily control of Stage Two translation tables.

The verification effort
Nitro Isolation Engine was designed with verification in mind from the first line of code. Nitro Isolation Engine is subject to AWS’s existing rigorous engineering practices, including the deployment of property-based-testing and lightweight formal methods, for example the Kani bounded model checker for Rust [7].

Building atop this foundation, we have specified and verified the correctness of Nitro Isolation Engine in Isabelle/HOL [8]. Our model and proofs consist of around 260,000 lines of machine-checked models and proofs. Specifically, we have proved:

Functional correctness: Nitro Isolation Engine behaves as specified for all operations: virtual machine creation, memory mapping, instruction and data abort handling, and so on. As corollaries of our total verification style, we have also proven memory-safety, termination, and absence of runtime errors, providing our modelling assumptions are accurate.
Confidentiality: We prove a noninterference-style property demonstrating the confidentiality of guest virtual machine states, formalized as indistinguishability preservation up-to permitted flows of declassified information out of a guest.
Integrity: The integrity of guest virtual machine state is formalized as a safety property, showing that the private state of one virtual machine is unaffected by operations modifying another distinct virtual machine.
In addition, we have applied Iris [9] and Verus [10] to prove the correctness of the Nitro Isolation Engine’s concurrency primitives, including ticket locks, mutexes, and rendezvous barriers.

For functional verification, we defined μRust, a restricted subset of Rust expressive enough to write Nitro Isolation Engine but amenable to formal reasoning and embedded its semantics into Isabelle/HOL. Specifications are written in separation logic, and proofs proceed via weakest precondition calculus with custom automation. We have made our verification infrastructure open source as the AutoCorrode library [11] for Isabelle/HOL, which may be of independent interest.

Regards,
Automated Reasoning Group, AWS

[1]: https://www.aboutamazon.com/news/aws/aws-graviton-5-cpu-amazon-ec2
[2] : https://www.youtube.com/watch?v=3Gt-30Fm38U https://www.youtube.com/watch?v=3Gt-30Fm38U
[3]: https://www.youtube.com/watch?v=b0P55gHhG4g
[4]: https://sel4.systems/
[5]: https://flint.cs.yale.edu/certikos/
[6]: https://www.usenix.org/conference/usenixsecurity21/presentation/li-shih-wei
[7]: https://github.com/model-checking/kani
[8]: https://isabelle.in.tum.de/
[9]: https://iris-project.org/
[10]: https://github.com/verus-lang/verus
[11]: https://github.com/awslabs/AutoCorrode

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

Very funny! And pretty exciting too. 😁

https://www.producthunt.com/products/ecosort-2

Potentially useful, but it seems to send your pictures of garbage to Google Gemini. On the other hand, sending garbage to Google Gemini sounds pretty fun even without recycling. 😏

https://openai.com/index/shipping-sora-for-android-with-codex/

Очень умилительный пост. 😊 По итогу OpenAI выяснили, что можно очень быстро написать небольшое приложение с очень высоким уровнем качества, если

— собрать небольшую команду очень квалифицированных инженеров
— не заёбывать их процессами и бюрократией
— тщательно продумать и зафиксировать архитектуру приложения
— на ранней стадии реализовать end-to-end несколько наиболее критичных фич
— методично покрывать всё тестами
— делать (detailed) design review прежде чем кидаться кодить

Это, безусловно, прорыв. Никто до них такого не знал. (Peopleware? Джоэл Спольски? Не, не слышал.)

Для меня загадочными остались только два вопроса:

1. зачем в этой схеме Codex?
2. что ж мешало всем так делать последние ~40 лет?

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

In the essence, it's just a one cool fancy example of probabilistic programming... but it's still cool, though-provoking and kinda deep in more that one way.

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

A sorta follow-up. Behind the Scenes, a breakdown of the process, the lighting, the props and so on. A must-watch for anyone shooting anything. A lot of tips, tricks and wisdom.

ARMA 5 is already here, you're simply looking in the wrong store! 😂

https://nibblestew.blogspot.com/2023/09/circles-do-not-exist.html

Old news: Circles do not exist... in PDF, apparently. 😁

Случайно купил молотый кофе в такой же пачке, в каких продают зёрна. Пять минут не мог понять, как же его заваривать — кофемолка, очевидно, бесполезна, но с чего тогда начинать, если не с помола?

По итогу оказался вполне неплохой кофе. По крайней мере, пока он свежий. Хотя помол мелковат для воронки, на мой вкус. И много "шелухи" в помоле.

The famous Jeff Dean and Sanjay Ghemawat recently (2025/12/16) updated their quite elaborate and comprehensive article on performance engineering:
https://abseil.io/fast/hints.html