Здравствуйте, kochetkov.vladimir, Вы писали:

Я тут говорил про верификацию safety. Ты же расширил тему на верификацию вообще всего. И ещё security притянул о которой речи вообще не шло.
При этом нужно всегда помнить, что без safety о security разговор можно даже не начинать.
И safety сама по себе является очень полезной штукой даже без security.

KV>Её и не должно быть в коде. ... Всё это вместе и составляет первую часть той модели, о которой я говорил.
К счастью для того о чём говорю я это всё не нужно.

KV>И это уже делает HTTP контекстно-зависимым языком (см. https://pdfs.semanticscholar.org/7d95/6ddef192f3a10b22bc41044566be396c751f.pdf, п3.3), для разбора которого требуется LBA, суть -- машина Тьюринга с ограниченной памятью.
Как это мешает верифицировать две простейшие функции?
Тут же всё намного проще чем сортировка.

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

KV>Для верификации криптографии, кстати, на практике используются специально заточенные под эту задачу DSL'и. Такие, как https://github.com/GaloisInc/cryptol, например. Просто потому, что описать даже примитивные криптоалгоритмы традиционными средствами верификации невероятно тяжело.
Я посмотрел по диагонали. Но ничего необычного кроме манипуляции последовательностями бит там не увидел.
Прямая поддержка этой фичи действительно сильно упрощает жизнь. Причём не только верификатору, но разработчикам алгоритмов. И потенциально из этого описания можно генерировать очень быстрый код.