Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

F* и Agda/Coq

На днях я рассказывал о тяготах программирования сложных вещей на Агде: дела в самом деле обстоят так, что я, не смотря на более чем 10-15 (смотря как считать) лет опыта в машинной верификации и валидации, периодически чувствую себя слишком тупым, чтобы на этом писать:
Проблема в том, что придумать конструкции, корректные по построению. А упираешься в то, что заведомо верно работающий код никак не хочет, например, проходить фазу проверки на отсутствие бесконечного зацикливания, и нет никаких подсказок, почему не хочет. Или есть, но сообщения об ошибках написаны недоступным для человеческого понимания образом. И нужно отгадать и переформулировать. Так, чтобы бездушная машина врубилась.

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

Так вот, на самом деле я считаю, что нет. Я считаю, что для нужд “реального программирования” (исключая местами написание инфраструктурных библиотек) почти всегда удобнее использовать не корректность по построению, а корректность, проверяемую пост-фактум, причём работу по доказательству корректности (или поиску контрпримера) должен насколько это только возможно, перенимать “искусственный интеллект”.

Для реального программирования с контрактами и машинной проверкой корректности на данный момент лучшим является F* (https://www.fstar-lang.org/tutorial/):
– берётся нормальный императивный языка программирования с очень сильной поддержкой функциональщины и ООП (или, если угодно, нормальный функциональный язык с очень сильной поддержкой императивщины и капсюляции изменяемого состояния),
– к нему прикручивается мощная система типов с инструментарием для ограничения побочных эффектов у процедур и контрактов: требований и гарантий для процедур, инвариантов для структур данных и объектов с изменяемым состоянием, локальных и глобальных гарантий для взаимодействующих систем, и
– мощный солвер (в данном случае мощнейший SAT-Solver Z3), который берёт на себя работу по автоматическому доказательству всего, что доказывается тривиально.

Почему же тогда я занимаюсь вещами в ключе Agda, а не в ключе F*? Дело в том, что для того чтобы при помощи F* можно было сделать всё, что хочется делать, сперва нужен достаточно развитый _язык_ для описания тех самых контрактов, требований и гарантий, а также для определения сложнейших с вычислительной точки зрения типов данных, таких как вещественные числа неограниченной точности, взаимодействующие распределённые системы и внешние объекты (в смысле линейных типов).

Создание/доведение достаточного для всех практических и математических задач логического исчисления и языка/proof assistant'а на базе такой теории. Это первый шаг к созданию такого (аналога) F*, на котором будет удобно писать всевозможный софт, для которого есть потребность в верификации и валидации, в т.ч. ядра операционных систем, стеки сетевых протоколов, компиляторы, криптографию, распределённые системы и числодробилки, а также любые библиотеки, фреймворки, сервисы и платформы, предназначенные для широкого использования.
К счастью, второй и третий шаг на этом пути уже сделали создатели F*: они подали пример, как к достаточно приземлённому языку приделать контракты произвольной сложности, и как прикрутить к этому ”искусственный интеллект”, справляющийся с автоматическим доказательством тривиальных вещей в довольно широком разнообразии случаев.
Следующим шагом, по видимому, будет прикручивание ко всему этому ещё и солверов на базе нейронных сеток, которые будут справляться с нетривиальными, но укладывающимися в рамки распространённых подходов случаями. Успехи Machine Learning в последние годы позволяют надеяться, что эта задача будет для них посильна.
Subscribe
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 20 comments