F* — жемчужина зависимых типов

первая часть

Неужели F* в этой промежуточной нише такой один? Нет, вот его некоторые конкуренты:

— ATS (Applied Type System) — язык программирования для стыковки программного кода с формальными спецификациями. В нём довольно хитро комбинируются механизмы теорем прувинга с классическим программированием на базе мощной системы типов. При этом производительность его сравнима с кодом на Си, но компилятору удаётся фиксировать ошибки деления на ноль, утечки памяти, переполнения буфера и т. п.

— Idris (no comments);

— различные применения по теме логики Хоара (точнее, её расширения — Hoare Type Theory, HTT), реализаций коей немало на гитхабе;

— Trellys — оригинальная технология с полной поддержой зависимых типов, идея которой — создавать языки, в которых единообразно поддерживался бы как функциональный стиль программирования, так и разработка в зависимых типах.

Но! На сегодня только F* сочетает а) зависимые типы, б) механизм SMT-солверов, в) прикладное функциональное программирование в духе ML и Hackell ! На практике F*, конечно, опенсорсный, реализован для всех основных платформ.

Вот как это выглядит:

а) F* реализован на F*, а компилируется в F# или OCaml (или даже Си);
б) на F* в стиле SMT верифицированы реализации протокола TLS;
в) мета-теория F* (частично) формализована на F*, который используется и как пруф-ассистент.

Более того, программы в зависимых типах сами можно использовать как доказательства — обычные SMT-солверы тут ломаются. F* даже позволяет выбирать различные представления моделей памяти.

F* при поддержке Microsoft развивается весьма активно, планы развития открыты, документация весьма полная и подробная, поэтому всем, интересующимся программированием в зависимых типах и системами типа Idris или Coq, хочу порекомендовать именно F* — и как стартовый язык для погружения в тему, и как развитый механизм для решения соответствующих прикладных задач.

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

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

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