Хабрахабр

[Перевод] Если вы не пишете программу, не используйте язык программирования

Это он впервые, ещё в 1979 году, ввёл понятие последовательной согласованности, а его статья «How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs» получила премию Дейкстры (точней, в 2000 году премия называлась по-старому: «PODC Influential Paper Award»). Лесли Лэмпорт — автор основополагающих работ в распределённых вычислениях, а ещё вы его можете знать по буквам La в слове LaTeX — «Lamport TeX». Если вы в восторге от решения задач на happens-before или проблемы византийских генералов (BFT), то должны понимать, что за всем этим стоит Лэмпорт. Про него есть статья в Википедии, где можно добыть ещё несколько интересных ссылок.

В докладе пойдёт речь о формальных методах, применяемых в разработке сложных и критичных систем вроде космического зонда Rosetta или движков Amazon Web Services. Эта хабрастатья — перевод доклада Лесли на Heidelberg Laureate Forum в 2018 году. На этом вступление закончено, мы передаём слово автору. Просмотр этого доклада является обязательным для посещения сессии вопросов и ответов, которую проведет Лесли на конференции Hydra — эта хабрастатья может сэкономить вам час времени на просмотр видео.

Я бы это перефразировал так: «В каждой большой программе живет алгоритм, который пытается выбраться наружу». Когда-то давно Тони Хоар написал: «В каждой большой программе живет маленькая программа, которая пытается выбраться наружу». Не знаю, правда, согласится ли с такой интерпретацией Тони.

В этом алгоритме мы присваиваем $x$ значение $M$, $N$ — значение $y$, и затем отнимаем наименьшее из этих значений от наибольшего, пока они не оказываются равны. Рассмотрим в качестве примера алгоритм Евклида для нахождения наибольшего общего делителя двух положительных целых чисел $(M, N)$. В чем существенное отличие этого алгоритма и программы, которая его реализует? Значение этих $x$ и $y$ и будет наибольшим общим делителем. Четкой разницы между алгоритмами и программами нет, но на интуитивном уровне мы чувствуем отличие — алгоритмы более абстрактные, более высокоуровневые. В такой программе будет много низкоуровневых вещей: у $M$ и $N$ будет определенный тип, BigInteger или что-то в таком роде; нужно будет определить поведение программы в случае, если $M$ и $N$ неположительные; и так далее и тому подобное. Обычно это не те алгоритмы, про которые нам рассказывали в курсе алгоритмов. И, как я уже сказал, внутри каждой программы живет алгоритм, который пытается выбраться наружу. Чаще всего он будет значительно сложнее тех, которые описаны в книгах. Как правило, это алгоритм, который полезен только для данной конкретной программы. И в большинстве случаев выбраться наружу этому алгоритму не удается, потому что программист не подозревает о его существовании. Такие алгоритмы зачастую называют спецификациями. Программу, написанную таким образом, сложно отлаживать, поэтому что это значит отлаживать алгоритм на уровне кода. Дело в том, что этот алгоритм нельзя увидеть, если ваше мышление сосредоточено на коде, на типах, исключениях, циклах while и прочем, а не на математических свойствах чисел. Кроме того, такая программа будет неэффективной, потому что, опять-таки, вы будете оптимизировать алгоритм на уровне кода. Средства отладки предназначены для того, чтобы находить ошибки в коде, а не в алгоритме.

Для этого существует много способов, мы рассмотрим наиболее полезный из них. Как и почти в любой другой области науки и техники, решить эти проблемы можно, описав их математически. Заключается этот метод в том, чтобы описать выполнение алгоритма как последовательность состояний, а каждое состояние — как присвоение свойств переменным. Он работает как с последовательными, так и с параллельными (распределенными) алгоритмами. Затем мы отнимаем меньшее значение от большего ($x$ от $y$), что приводит нас к следующему состоянию, в котором мы отнимаем уже $y$ от $x$, и на этом выполнение алгоритма останавливается: $[x \leftarrow 12, \leftarrow 18], [x \leftarrow 12, \leftarrow 6], [x \leftarrow 6, \leftarrow 6]$. Например, алгоритм Евклида описывается как последовательность следующих состояний: вначале x присваивается значение M (число 12), а y — значение N (число 18).

Тогда любой алгоритм можно описать множеством поведений, которые представляют все возможные варианты выполнения алгоритма. Назовем последовательность состояний поведением, а пару последовательных состояний — шагом. У более сложных алгоритмов, в особенности параллельных, множества поведений большие. Для каждого конкретного M и N есть только один вариант выполнения, поэтому для его описания достаточно множества из одного поведения.

Некоторое поведение $s_1, s_2, s_3 ...$ входит в множество поведений только если начальный предикат верен для $s_1$, и предикаты следующего состояния верны для каждого шага $(s_i, s_)$. Множество поведений описывается, во-первых, начальным предикатом для состояний (предикат — это просто функция с булевым значением); и, во-вторых, предикатом следующего состояния для пар состояний. Начальный предикат здесь такой: $(x = M)\land(y = N)$. Попробуем описать таким образом алгоритм Евклида. А предикат следующего состояния для пар состояний здесь описывается следующей формулой:

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

После логического И утверждается, что значение x во втором состоянии равно значению x в первом состоянии минус значение y в первом состоянии. Как видим, первая строка гласит, что в первом случае x больше y в первом состоянии. Все это значит, что в случае, когда x больше y, программа отнимет y от x, а y оставит неизменным. После еще одного логического И утверждается, что значение y во втором состоянии равно значению y в первом состоянии. Обратите внимание, что эта формула ложна, если x равен y. Последние три строки описывают случай, когда y больше x. В этом случае следующего состояния нет, и поведение останавливается.

Что может быть прекраснее этих двух формул? Итак, мы только что описали алгоритм Евклида двумя математическими формулами — и нам не пришлось связываться ни с каким языком программирования. Поведение $s_1, s_2, s_3 ...$ является выполнением алгоритма Евклида только в том случае, если: Заменить их одной формулой.

  • $Init_E$ верно для $s_1$,
  • $Next_E$ верно для каждого шага $(s_i, s_{i+1})$.

Первое условие можно выразить просто как $Init_E$. Записать это как предикат для поведений (будем называеть его свойством) можно следующим образом. Второе условие записывается так: $\square Next_E$. Это значит, что мы интерпретируем предикат состояния как верный для поведения только в том случае, если он верен для первого состояния. В итоге формула выглядит так: $Init_E\land\square Next_E$. Квадрат означает соответствие между предикатами пар состояний и предикатами поведений, то есть $Next_E$ верно для каждого шага в поведении.

В сущности, это просто определения, или сокращения для $Init_E$ и $Next_E$. Итак, мы записали алгоритм Евклида математически. Полностью эта формула выглядела бы так:

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

При $M = 12$ и $N = 18$ они верны для следующего поведения: $[x \leftarrow 12, \leftarrow 18], [x \leftarrow 12, \leftarrow 6], [x \leftarrow 6, \leftarrow 6]$. Свойство, которое мы записали, верно для некоторого поведения только в том случае, если выполняются два условия, которые мы только что описали. А их мы не должны учитывать, поскольку это просто отдельные шаги уже учтенного нами поведения. Но эти условия также выполняются для более коротких версий того же поведения: $[x \leftarrow 12, \leftarrow 18], [x \leftarrow 12, \leftarrow 6]$. Но это не совсем правильный подход, нам нужно более общее решение. Есть очевидный способ от них избавиться: просто не учитывать поведения, которые заканчиваются состоянием, для которого возможен хотя бы один следующий шаг. Кроме того, такое условие не всегда работает.

Свойство безопасности указывает, какие события допустимы. Обсуждение этой проблемы приводит нас к понятиям безопасности и активности. Свойство активности указывает, какие события должны рано или поздно произойти. Например, алгоритму разрешается вернуть правильное значение. Для алгоритма Евклида свойство безопасности выглядит следующим образом: $Init_E \land \square Next_E$. Например, алгоритм рано или поздно должен вернуть некоторое значение. В языках программирования в лучшем случае есть некоторое примитивное определение активности. К этому необходимо добавить свойство активности, чтобы исключить преждевременные остановки: $Init_E \land \square Next_E \land L$. И чтобы добавить это свойство, нужен довольно замысловатый код. Чаще всего активность даже не упоминается, просто подразумевается, что следующий шаг в программе обязательно должен произойти. Математически же активность выразить очень легко (как раз для этого нужен тот квадратик), но, к сожалению, у меня на это нет времени — нам придется ограничить наше обсуждение безопасностью.

Для каждого множества последовательностей существует естественная топология, которую создает следующая функция расстояния: Небольшое отступление только для математиков: каждое свойство является множеством поведений, для которых это свойство верно.

$s = 17, \sqrt{2}, -2, \pi, 10, 1/2\\ t = 17, \sqrt{2}, -2, e, 10, 1/2$

Соответственно, чем более продолжителен участок, на котором эти последовательности идентичны, тем ближе они друг к другу. Расстояние между этими двумя функциями — ¼, поскольку первое различие между ними — на четвертом элементе. В этой топологии свойства безопасности являются замкнутыми множествами, а свойства активности являются плотными множествами. Сама по себе эта функция не так уж и интересна, но она создает очень интересную топологию. Если вспомнить, что свойства — это множества поведений, то из этой теоремы следует, что каждое свойство является конъюнкцией свойства безопасности и свойства активности. В топологии одна из фундаментальных теорем гласит, что каждое множество является пересечением замкнутого множества и плотного множества. Это вывод, который будет интересен в том числе и программистам.

Частичная корректность алгоритма Евклида гласит, что если он завершил выполнение, то $x = GCD(M, N)$. Частичная корректность означает, что программа может остановиться только в том случае, если выдаст правильный ответ. Иначе говоря, $(x = y) \Rightarrow (x = GCD(M, N))$. А завершает выполнение наш алгоритм в случае, если $x = y$. Добавим в ее начало символ $\square$, который означает «для всех шагов». Частичная правильность этого алгоритма означает, что эта формула верна для всех состояний поведения. А если нечто верно для первого состояния каждого шага, то это утверждение верно для всех состояний. Как видим, в формуле нет переменных со штрихом, так что ее истинность зависит от первого состояния в каждом шаге. Как мы видели, поведение допустимо в том случае, если истинна только что приведенная формула. Частичная корректность алгоритма Евклида удовлетворяется любым поведением, допустимым для алгоритма. Не правда ли, это прекрасно? Когда мы говорим, что свойство удовлетворено, это просто значит, что это свойство следует из некоторой формулы. Вот она:

$Init_E\land\square Next_E \Rightarrow \square((x = y) \Rightarrow (x = GCD(M, N)))$

Квадрат со скобками после него называется свойство инвариантности: Перейдем к инвариантности.

$Init_E\land\square Next_E \Rightarrow \color{red}{\square((x = y) \Rightarrow (x = GCD(M, N)))}$

Значение, заключенное в скобки после квадрата, называется инвариант:

$Init_E\land\square Next_E \Rightarrow \square(\color{red}{(x = y) \Rightarrow (x = GCD(M, N))})$

Чтобы доказать $Init_E\land\square Next_E \Rightarrow \square I_E$, нужно доказать, что для любого поведения $s_1, s_2, s_3 ...$ следствием $Init_E\land\square Next_E$ является истинность $I_E$ для любого состояния $s_j$. Как доказать инвариантность? Мы можем доказать это методом индукции, для этого нам необходимо доказать следующее:

  1. из $Init_E\land\square Next_E$ следует, что $I_E$ верно для состояния $s_1$;
  2. из $Init_E\land\square Next_E$ следует, что если $I_E$ верно для состояния $s_j$, то оно также
    верно для состояния $s_{j+1}$.

Поскольку формула утверждает, что $Init_E$ верно для первого состояния, это значит, что $I_E$ верно для первого состояния. Вначале нужно доказать, что $Init_E$ подразумевает $I_E$. Это записывается так: $Next_E \land I_E \Rightarrow I'_E$, где $I'_E$ — это $I_E$ для всех переменных со штрихом. Далее, при $Next_E$, верном для любого шага, и $I_E$, верном для $s_j$, $I_E$ верно для $s_{j+1}$, потому что $\square Next_E$ значит, что $Next_E$ верно для любой пары состояний.

Частичная корректность не индуктивна. Инвариант, отвечающим двум условиям, которые мы только что доказали, называется индуктивным инвариантом. В нашем случае индуктивный инвариант будет такой: $GCD(x, y) = GCD(M, N)$. Чтобы доказать ее инвариантность, нужно найти индуктивный инвариант, который ее подразумевает.

Алгоритм удовлетворяет свойству безопасности, поскольку в нем сохраняется индуктивный инвариант. Каждое следующее действие алгоритма зависит от его текущего состояния, а не от прошлых действий. е. Алгоритм Евклида может вычислить наибольший общий знаменатель (т. Чтобы понять алгоритм, необходимо знать его индуктивный инвариант. он не останавливается, пока его не достигнет) благодаря тому, что в нем есть инвариант $GCD(x, y) = GCD(M, N)$. Возможно, вы также слышали о методе Овики-Грис, который является распространением метода Флойда-Хоара на параллельные программы. Если вы изучали верификацию программ, то вы знаете, что только что приведенное доказательство инварианта — это ни что иное, как метод доказательства частичной корректности последовательных программ Флойда-Хоара. И если это делать при помощи математики, а не языка программирования, это делается предельно просто. В обоих случаях индуктивный инвариант пишется при помощи аннотации программы. Математика делает сложные явления значительно доступнее для понимания, хотя сами явления, конечно же, от этого не станут проще. Именно это лежит в основе метода Овики-Грис.

Если в математике мы написали формулу с переменными $x$ и $y$, это не значит, что других переменных не существует. Взглянем подробнее на формулы. Просто формула ничего не говорит ни о каких других переменных. Можно добавить еще одно уравнение, в котором $y$ поставлено в отношение к $z$, это ничего не поменяет. Должен признаться: когда я сказал, что формула $Init_E\land\square Next_E$ описывает алгоритм Евклида, я соврал. Я уже говорил, что состояние — это присвоение значений переменным, сейчас к этому можно добавить: всем возможным переменным, начиная $x$ и $y$ и заканчивая населением Ирана. Вторая часть формулы ($\square Next_E$) утверждает, что каждый шаг изменяет $x$ или $y$. На самом деле она описывает вселенную, в которой значения $x$ и $y$ представляют выполнение алгоритма Евклида. Из этого следует, что в Иране никто не может родиться после того, как завершено выполнение алгоритма Евклида. Иначе говоря, она описывает вселенную, в которой население Ирана может измениться только в том случае, если изменилось значение $x$ или $y$. Исправить эту ошибку можно в том случае, если у нас допустимы шаги, для которых $x$ и $y$ остаются неизменными. Очевидно, это не так. Для краткости запишем это так: $Init_E \land \square [Next_E]_{<x,y>}$. Поэтому к нашей формуле нужно добавить еще одну часть: $Init_E \land \square (Next_E \lor (x' = x) \land (y' = y))$. Те же изменения нужно внести в доказательство инварианта: Эта формула описывает вселенную, содержащую алгоритм Евклида.

  • Доказываем: $Init_E \land \color{red}{\square [Next_E]_{<x,y>}} \Rightarrow \square I_E$
  • С помощью:
    1. $Init_E \Rightarrow I_E$
    2. $\color{red}{\square [Next_E]_{<x,y>}} \land I_E \Rightarrow I'_E$

Исключить такие поведения нужно с помощью свойства активности. Это изменение отвечает за безопасность алгоритма Евклида, поскольку теперь возможны поведения, в которых значения $x$ и $y$ не изменяются. Это сделать довольно просто, но сейчас я про это говорить не буду.

Предположим, у нас есть некоторая машина, которая реализует алгоритм Евклида подобно компьютеру. Поговорим о реализации. Для простых операций сложения и вычитания ей нужно множество шагов, как компьютеру. Она представляет числа как массивы 32-битных слов. Что мы подразумеваем, когда говорим, что машина Евклида реализует алгоритм Евклида? Если пока не трогать активность, то такую машину мы также можем представить формулой $Init_{ME} \land \square [Next_{ME}]_{<...>}$. Это значит, что следующая формула верна:

Она гласит, что наша машина удовлетворяет некоторому свойству ($\Rightarrow$). Не пугайтесь, мы сейчас рассмотрим ее по порядку. Иначе говоря, вторая строка — это формула Евклида, в которой $x$ и $y$ заменены на выражения в многоточиях. Этим свойством является формула Евклида $(Init_E \land \square [Next_E]_{<х,у>}$, многоточия — это выражения, которые содержат переменные машины Евклида, а $WITH$ — это подстановка. По сути, формула Евклида ($Init_E \land \square [Next_E]_{<х,у>}$) — это сокращение для формулы: В математике нет общепринятого обозначения подстановки, поэтому мне пришлось придумать его самому.

Красным выделена часть формулы, позволяющая $x$ и $y$ в $(Init_E \land \square [Next_E]_{\color{red}{<х,у>}}$ оставаться неизменными.

Если просто взять пару программ и сказать, что переменные этих программ связаны с $x$ и $y$ — бессмысленно говорить, что всё это «реализует алгоритм Евклида». Описанное выражение утверждает не только, что машина реализует алгоритм Евклида, но и что она делает это с учетом указанных подстановок. Сейчас у меня нет времени, чтобы показать, что описанное выше определение является правильным, вам придется поверить мне на слово. Обязательно указать, как именно алгоритм будет реализован, почему после всех подстановок формула станет истинной. Математика действительно прекрасна — при помощи нее мы смогли определить, что значит, что один алгоритм реализует другой. Но вы, я думаю, уже оценили, насколько оно простое и элегантное.

Для этого необходимо выполнить следующие условия: Чтобы доказать это, необходимо найти подходящий инвариант $I_{ME}$ машины Евклида.

  1. $Init_{ME} \Rightarrow (Init_E, WITH\thinspace x\leftarrow ..., y \leftarrow ...)$
  2. $I_{ME} \land [Next_{ME}]_{<...>} \Rightarrow ([Next_E]_{<х,у>}, WITH\thinspace x\leftarrow ..., y \leftarrow ...)$

Инвариант $I_ {ME}$ объясняет, почему машина Евклида реализует алгоритм Евклида. Не будем сейчас в них вникать, просто обратите внимание на то, что это обычные математические формулы, хоть и не самые простые. Это вполне обычная математическая операция. Реализация означает подстановку выражений на место переменных. Нельзя подставить a + b на место x в выражении присвоения x = …, такая запись не будет иметь смысла. Но в программе такую подстановку выполнить невозможно. Если вы думаете только в рамках программирования — это невозможно. Тогда как определить, что одна программа реализует другую? Перевести программу в математическую формулу значит дать программе семантику. В лучшем случае вы сможете найти какое-нибудь мудреное определение, но гораздо более хороший способ — перевести программы в математические формулы и использовать определение, которое я привел выше. Языки программирования очень сложные, поэтому этот перевод программы на язык математики тоже сложный, так что на практике мы так не делаем. Если машина Евклида является программой, а $Init_{ME} \land \square [Next_{ME}]_{<...>}$ — ее математическая запись, то $(Init_E \land \square [Next_E]_{<х,у>}, WITH\thinspace x\leftarrow ..., y \leftarrow ...)$ показывает нам, что это значит, что «программа реализует алгоритм Евклида». Важность приведенного примера в том, что математика здесь показывает, что нужно сделать, чтобы реализовать алгоритм Евклида в программе: нужно определить, как x и y представлены в терминах состоянии программы и рассказывает, и что нужно дальше делать. Просто языки программирования не предназначены для того, чтобы писать на них алгоритмы. Но, конечно, в первую очередь, для написания алгоритмов не стоит использовать язык программирования.

На самом деле, это так только кажется. Кто-то обязательно скажет: математика работает на мелких выдуманных примерах, все знают, что в реальном мире программистам приходится иметь дело с огромными системами, и там от нее нету толку. Вместо шести строк предикат следующего состояния может занимать несколько сотен или тысяч строк. Единственное отличие алгоритма Евклида и большого алгоритма — это размер формулы. В программировании есть множество мудреных методов для этого, но самый простой и мощный метод — математический, и этот способ называется определение. Для таких больших формул мы используем иерархическую декомпозицию, так мы боремся со сложностью. Чтобы выполнить иерархическую декомпозицию вот этой формулы:

Назовём вот эту часть $DecrementX$: мы даем имена частям этой формулы.

а вот эту часть — $DecrementY$:

Поэтому можно сказать, что:

Проще определений ничего не придумать.

Rosetta — космический зонд, сделанный Европейским космическим агентством для исследования одной кометы. Поговорим о реальных примерах математического описания алгоритмов. Ее создатели затем сделали следующую версию этой системы и написали о ней книгу. Некоторые ее инструменты управлялись операционной системой реального времени Virtuoso. Он работает по тем же принципам, что и примеры, которые я приводил в этом докладе. Высокоуровневая структура там описана на TLA+, это язык для математической записи алгоритмов. Я спросил его, принес ли им пользу TLA+, на что он ответил: «Во многом благодаря TLA+ нам удалось создать значительно более чистую архитектуру. Процитирую отрывок из письма, которое мне прислал Эрик Верхольст (Eric Verhulst), он руководил разработкой системы. Одним из результатов использования TLA+ стало уменьшение размера кода в десять раз по сравнению с Virtuoso». Нам стали видны последствия многолетней промывки мозгов из-за программирования на C. Просто качественным программированием сокращения кода в десять раз не достичь. Вдумайтесь в эту цифру. А для этого нужно математическое мышление. Для этого нужна более чистая архитектура, или, другими словами, более совершенный алгоритм. Если вы мыслите в рамках языка программирования, такого результата вам не достичь. А к математическому мышлению приучает TLA+.

В Communications of the ACM несколько лет тому назад была ]опубликована статья о том, как веб-сервисы Amazon используют формальные методы. Из космоса спустимся на облака. Формальный метод, о котором идет речь — это всё тот же TLA+. Amazon Web Services — это те, кто создают облачную инфраструктуру Amazon. Во-первых, при помощи формальных методов удается найти баги в структуре системы, которые невозможно обнаружить никаким другим известным авторам способом. Основные выводы статьи следующие. Во-вторых, по их мнению, формальные методы на удивление легко приживаются с общепринятыми методами разработки ПО и отлично окупаются. Подчеркну, это пишут программисты, которые в течение долгого времени занимаются распределенными системами. В-третьих, статья сообщает нам, что в Amazon формальные методы систематически применяются для проектирования сложных программ, включая публичные облачные сервисы. Нужно сказать, что авторы — люди, которые не витают в облаках, они привыкли оценивать технологии в долларовом эквиваленте. Мне недавно говорили, что около 10% программистов в этих группах используют TLA+.

Эпизодически там TLA+ применяется начиная с 2004 года. Другой пример — Microsoft. ч. В конце 2015 года я написал короткую статью про TLA+, в которой было описано в т. Эту статью прочитал генеральный директор Microsoft Сатья Наделла, и на следующий день после рождества того года он отправил письмо высшему руководству компании, в котором рекомендовал им также познакомиться с этой статьёй. его применение в Amazon Web Services. К счастью, в Microsoft по-прежнему пост генерального директора занимает бывший программист. Приведу цитату: «С учетом сложности параллельных распределенных систем мы должны обеспечить корректность алгоритмов на уровне проектирования, в противном случае у нас возникнут проблемы в будущем». В 2016-17 гг. Дальше он пишет: «Нам следует постараться вдохновить как можно больше программистов на использование этих методов». Два менеджера из Azure сделали презентацию на семинаре в апреле 2018 года, в которой говорилось, что сложные системы требуют строгого математического мышления на каждом этапе их разработки. я провел три трёхдневных курса по TLA+, их прошли около 150 программистов, в основном работавших на Azure (облачная платформа Microsoft). Но если вы ее не продумываете, вы гарантированно сделаете ошибки». Они цитировали меня: «Продумывание задачи не гарантирует, что вы не совершите ошибок. И здесь опять-таки на помощь приходит математика: код хорош для написания системы, но для ее среды необходимо нечто более простое и выразительное. В презентации также говорилось о необходимости моделировать систему целиком, то есть всю вселенную, которая включает систему и ее среду. В заключение было сказано, что нужно мыслить математически, и что многие программисты этого не делают.

Этого он предлагал достичь, нанимая программистов с опытом работы в TLA+, интегрируя тренинги по TLA+ в курс адаптации новых программистов и в курс учебного лагеря Azure, и требуя, чтобы каждый анализ причин багов корректности в продакшне сопровождался спецификацией на TLA+. Процитирую другого менеджера, который говорил о необходимости интегрировать TLA+ в культуру программирования. Наконец, автор также говорил о необходимости требовать спецификацию на TLA+ для гарантий, которые заявляет сервис. Последняя мера гарантирует, что человек понял первопричину бага. Насколько мне известно, этот проект пока что очень успешен. Сегодня Microsoft выпускает новую версию Cosmos DB, это глобальная база данных, от которой в значительной степени будет зависеть будущее всей компании. В его разработке использовался TLA+, и гарантии условий правильности, предоставляемые пользователям, сопровождаются в нем спецификациями на TLA+.

В нем есть мощные инструменты для проверки свойств инвариантности и активности и их реализации. TLA+ — это язык для математического описания алгоритмов. Для начала, не все алгоритмы стоят того, чтобы их описывать на полностью формальном языке. Но TLA+ не является лучшим языком для описания всех возможных алгоритмов. Но главное другое: опыт TLA+ доказывает, что математическое описание алгоритмов работает на практике. Инструменты TLA+ не подходят для многих областей, они лучше всего работают с распределенными системами.

И прежде, чем начинать писать программу, нужно найти и понять этот алгоритм. В каждой большой программе живет алгоритм, который пытается выбраться наружу. Если алгоритмы сложных распределенных систем в Amazon и Microsoft можно описать математически, то и с вашими алгоритмами это получится. А лучше всего это можно сделать, описав его математически. Не позволяйте языкам программирования промыть вам мозги, пусть математика освободит ваш разум.

Когда вы будете писать комментарии — помните, что автор их не прочитает. Напоминаю, что это перевод. Билеты можно приобрести на официальном сайте. Если вам действительно хочется пообщаться с автором, то он будет на конференции Hydra 2019, которая пройдёт 11-12 июля 2019 года в Санкт-Петербурге.

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть