Меню Главная Случайная статья Настройки F* Материал из https://ru.wikipedia.org F * (произносится как F star) — функциональный язык программирования, основанный на ML и ориентированный на формальную верификацию разрабатываемых на нём программ. Его система типов включает в себя зависимые типы, монадические эффекты и типы-уточнения[англ.]. Этих выразительных средств достаточно, чтобы задавать точные спецификации для программ, включая описания функциональной корректности и свойств безопасности. Механизм проверки типов в F* позволяет доказывать, что программы соответствуют их спецификациям. Это делается с использованием комбинации SMT-решателя и ручных доказательств. Программы, написанные на F*, могут быть странслированы в OCaml, F# и C для дальнейшей компиляции и выполнения. Предыдущие версии F* также можно было транслировать в JavaScript. Последняя версия F* написана полностью на общем подмножестве F* и F# и может быть запущена как с использованием OCaml, так и с использованием F#. Исходный код языка открыт под лицензией Apache 2.0 и активно разрабатывается на GitHub[4]. Литература Ahman, Danel; Hricu, Ctlin; Maillard, Kenji; Martnez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). Dijkstra Monads for Free. 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Ссылки Домашняя страница F* Исходные коды F* на GitHub Учебник F* Примечания Microsoft Research Inria Joint Centre  (неопр.). MSR-INRIA. Дата обращения: 28 мая 2020. Архивировано 21 мая 2020 года. 1 2 https://www.fstar-lang.org/#people Release 0.9.6.0 — 2018. FStarLang/FStar  (неопр.). GitHub. Дата обращения: 28 мая 2020. Архивировано 10 июля 2020 года.