https://lamport.azurewebsites.net/tla/high-level-view.html
Никто не пишет фрагмент кода, не имея предварительно высокоуровневой модели того, что код должен делать и как он должен это делать. Программист никогда не начинает с того, что решает объявить какие-то переменные, добавляет оператор while , затем оператор if и т. д. Он только по завершении обнаруживает, что написал программу сортировки. Но программисты редко начинают с точной модели кода. Наличие только расплывчатой, неполной модели приводит к основным ошибкам проектирования, которые не исправит самый лучший код.
TLA+ — это язык для написания точных высокоуровневых моделей того, что делает код и как он это делает. Большинство программистов считают, что точные модели хороши только для крошечных четко определенных задач, таких как вычисление НОД, но бесполезны для реализации сложных систем. Они ошибаются. Чем сложнее система, тем важнее сделать ее максимально простой. В сложных системах простота не достигается хитростями кодирования. Это достигается строгим мышлением выше уровня кода.
В одном промышленном проекте , начиная с модели TLA+, размер кода операционной системы реального времени сократился в десять раз. Такое уменьшение размера кода не достигается более совершенным кодированием; это происходит из-за строгого мышления над уровнем кода.
Тестирование кода — неэффективный способ найти фундаментальные ошибки проектирования, особенно в параллельных и распределенных системах. Кроме того, ошибка проектирования, обнаруженная после того, как код был написан, обычно исправляется специальным патчем, который вряд ли устранит все экземпляры проблемы и, скорее всего, внесет новые ошибки. Ошибки проектирования следует выявлять путем написания точной высокоуровневой модели до того, как будет написан код.
ps
Определение систем: язык и инструменты TLA+
https://deep-econom.livejournal.com/1015564.html