Брутальный F*

F* — это функциональный язык (произносится «эф стар»), один из духовных наследников ML, исходно позиционировавшийся для задач автоматической верификации программ, а сегодня довольно успешно применяемый в ряде математических приложений и в качестве универсального языка (примерно как его младший собрат F#). Развивается он довольно стабильно, потому как поддерживается Microsoft Research.

Зачем Микрософту нужен ещё один функциональный F*, если уже есть очень хороший F#, давно встроенный в Visual Studio?

Дело в том, что применительно к задаче верификации функциональность функциональности рознь. Языки типа Лиспа или Хаскеля действительно излишне «универсальны», и применяются для верификации в основном модные ныне Agda, Coq иже с ними. Правильнее называть последние интерактивными пруф-ассистентами. Упомяну заодно в этой компании ещё такие системы:

— Bedrock — библиотека, которая превращает Coq в инструмент, схожий с классическими системами верификации (наподобие языка Boogie), что позволяет верифицировать код на низкоуровневых языках (например, ассемблере);
— CompCert — формально верифицированный оптимизирующий компилятор Си (стандарт C99), корректность которого была доказана с помощью Coq;
— Isabelle/HOL — теорем прувер с развитым интерфейсом,
поддерживающий запись доказательств в процедурном или декларативном стилях. Применялся для проектирования элементов серверов HP 9000;
— Lean — оригинальный теорем прувер, который позиционируется как потенциальный пруф-ассистент для гомотопической теории типов;
— seL4 — микроядро, корректность которого доказана автоматически (может использоваться в качестве гипервизора при запуске ядра Linux);

В чём их минус? Например, доказательство теоремы Feat-Thompson (любая конечная группа нечетного порядка разрешима) с помощью Coq заняло 170 тысяч строк кода! И хотя сам реализованный в этих пруверах математический механизм весьма гибок и выразителен, как функциональные языки эти системы почти никакие (правильнее их отнести к чистым функциональным языкам), что существенно усложняет процесс доказательства-программирования и приводит к упомянутым объёмам кода.

Существуют также и полуавтоматические верификаторы программ, которые весьма мощны именно в плане программирования. Вот примерный список лучших продуктов:

— Dafny — императивно-функциональный язык, поддерживающий спецификационные конструкции для описания предполагаемого поведения. Верификатор Dafny проверяет, что программы соответствуют их спецификациям;
— FramaC — фреймворк для модульного анализа Си-программ, инспектирующий код без выполнения оного;
— IronClad — хитрая система выполнения кода на удалённой машине с гарантией, что каждая его инструкция соответствует абстрактной спецификации  приложения;
— miTLS — верифицированная реализация протокола Transport Layer Security (TLS)на F#. Для проверки специальный тайп-чекер F7 (диалект ML);
— VCC — «механический», как его назвали авторы, верификатор параллельных Си-программ;
— VeriFast — экспериментальный прототип для верификации Си и Java-программ;
— Verve — экспериментальная верифицированная микрософтовская ОС, микроядро, над которым можно разворачивать «прикладную» ОС на C#.

Вот эта вторая группа, наоборот, предлагает мощные и богатые механизмы программирования, но, увы, поддерживает лишь логику типов первого порядка.

Таким образом, возник очевидный разрыв, и поэтому был придуман (ориентированный на верификацию конечно) достаточно общий язык с поддержкой систем типов высших порядков — в духе ML, но гораздо более предсказуемый в плане трудоёмкости программирования. F* реализует так называемую монадическую инкапсуляцию (когда в чистый функциональный код можно встраивать императивные куски, для чего требуется достаточно прозрачная модификация теории Хиндли-Милнера). Вдобавок в F* был добавлен механизм полуавтоматической верификации в стиле Dafny, но пожалуй самое главное, что в нём реализована поддержка индуктивных и зависимых типов, как в Agda/Coq!

вторая часть

Поделиться статьей ...Share on Facebook0Share on Google+0Tweet about this on TwitterShare on LinkedIn0Share on VKPrint this page

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

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