Как современные Ada-SPARK прокладывают путь к правильности через построение

Ответ Дейкстре: Как современные Ada/SPARK прокладывают путь к правильности через построение Запись трансляции конференции: Ada Developers workshop Прямой эфир состоялся 12 июня 2026 г. Дейкстра был одним из старейших и самых ярых сторонников подхода к программированию, основанного на принципе корректности по построению. Несмотря на многочисленные попытки, Дейкстра был разочарован промышленными вычислениями своего времени из-за недостаточного внимания к корректности. Его первоначальное впечатление от языка Ada во время его разработки также было довольно негативным в отношении его сложности. Он был не одинок: коллеги Дейкстры, такие как Хоар и Вирт, высказывали аналогичные претензии к Ada, несмотря на то, что были очень заинтересованы в этом языке. В этом докладе будет представлен краткий обзор этой истории, а затем даны ответы на эти критические замечания с помощью наглядных демонстраций. В целом, я планирую показать, что современный Ada/SPARK очень точно соответствует среде программирования, которую имели в виду Дейкстра и другие. Я сравню это с ограничениями других современных языков, таких как Lean4, при построении формально верифицированного программного обеспечения. В заключение, в докладе будут обобщены особенности Ada/SPARK, которые мы имеем сегодня и которые принимаются как должное. Докладчик: Меня зовут Дивья. В настоящее время я работаю независимым криптографом. Ранее я занималась формальной верификацией с использованием Lean4 и постквантовой криптографией. Я...