F* | |
---|---|
Класс языка |
мультипарадигменный: функциональное, объектно-ориентированное, обобщённое, императивное программирование |
Автор | Microsoft Research и INRIA[1] |
Разработчик | Microsoft Research[2] и 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[4].