F*

Не следует путать с F# — язык программирования.

F*
Класс языка	мультипарадигменный: функциональное, объектно-ориентированное, обобщённое, императивное программирование
Автор	Microsoft Research и INRIA
Система типов	строгая, статическая, с выводом типов, с зависимыми типами
Испытал влияние	Coq, Dafny, F#, Lean, OCaml, Standard ML
Лицензия	Apache Software License
Сайт	fstar-lang.org
ОС	Кроссплатформенное программное обеспечение (Linux, macOS, Windows)

F * (произносится как F star) — функциональный язык программирования, основанный на ML и ориентированный на формальную верификацию разрабатываемых на нём программ.

Его система типов включает в себя зависимые типы, монадические эффекты и типы-уточнения. Этих выразительных средств достаточно, чтобы задавать точные спецификации для программ, включая описания функциональной корректности и свойств безопасности. Механизм проверки типов в F* позволяет доказывать, что программы соответствуют их спецификациям. Это делается с использованием комбинации SMT-решателя и ручных доказательств. Программы, написанные на F*, могут быть странслированы в OCaml, F# и C для дальнейшей компиляции и выполнения. Предыдущие версии F* также можно было транслировать в JavaScript.

Последняя версия F* написана полностью на общем подмножестве F* и F# и может быть запущена как с использованием OCaml, так и с использованием F#. Исходный код языка открыт под лицензией Apache 2.0 и активно разрабатывается на GitHub.

Литература

• Dijkstra Monads for Free // 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. — 2017.

• Dependent Types and Multi-Monadic Effects in F* // 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. — 2016.

Ссылки

• Домашняя страница F*
• Исходные коды F* на GitHub
• Учебник F*