В мире распределённых систем есть инструменты, которые пугают с первого взгляда. TLA+ — один из них. Его боятся за формализм, математику и «академичность». Но именно поэтому его так любят инженеры из AWS, MongoDB и других компаний, где цена ошибки измеряется не багрепортами, а простоями дата-центров. В свежей заметке Мурат Демирбас — человек, который десятилетиями живёт в мире распределённых алгоритмов, — аккуратно объясняет: хорошая спецификация TLA+ начинается не с формул, а с правильного мышления...