Отдельно хочу прокомментировать эту новость. TLA⁺ — это язык спецификации, основанный на темпоральной логике действий, что позволяет описывать и верифицировать корректность распределенных систем, моделируя их поведение во времени. Есть отличный доклад от команды Elasticsearch о том, как они с помощью модели на TLA⁺ нашли и исправили ошибку, которая воспроизводилась только в сложных высококонкурентных сценариях. Это уже не «фантазии академиков в башнях из слоновой кости», а самый что ни есть реальный, прагматичный и прикладной способ повышать надежность ПО.
В общем, если вы занимаетесь распределенными системами или системами реального времени, есть смысл поучаствовать. Кто знает, вдруг через какое-то время на месте ребят из Elastic будете именно вы рассказывать, как улучшили ваш проект с помощью методов формальной верификации 😉