потихоньку развивается

инструменты становятся лучше

солверы прокачиваются

понемногу процесс упрощается

тут в чате есть более опытные ребята, про Coq можно поспрашивать

вообще в верификации есть разные направления, есть дедуктивная верификация, (это вот то что выше обсуждали), есть еще model checking. Если вкратце, то проверяется конечно автоматная модель программы на соответствие спецификации. Инструменты позволяют задавать предикаты над состоянием программы во времени (LTL), например какое-то условие выполняется только один раз и потом больше не выполняется. Инструментами можно верифицировать протоколы, проверять что нет дедлоков и тд. При этом, что интересно, инструмент может показать какие шаги привели к тому, что заданное условие перестало выполняться Много интересного есть 🙂

👍

из конкретных инструментов можно посмотреть например на SPIN http://spinroot.com/spin/whatispin.html и на TLA+ https://learntla.com/introduction/

TLA+ используют разработчики TiDB https://github.com/pingcap/tla-plus

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

интересно, при разработке николай дуров использует эти инструменты

у них же там своя криптография и тд
и много всего кастомного до костей

сидит небось в эклипсе и кодит на java сервер телеграма. Ну или сидит на диване и командует подручным разрабом, который сидит в эклипсе на джаве

а код на java как-то верифицируется?

И что такое вообще эти верификации и доказательства? Я пытался читать, не понял, пытался смотреть видео с разъяснениями, там человек очень гордо прочитал хеллоуворлд на си с добавлением отсебятины и сказал что его хеллоуворлд таким образом верифицирован

.. или доказан, не помню чего он пытался этим добиться

у телеги нет жавы в проде

и что ж у нее на серверах крутится?

плюсы и сишка

все по-старинке

серверы на си? Ну как-то....