F*

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

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

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

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

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

Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). “Dijkstra Monads for Free”. 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago (2016). “Dependent Types and Multi-Monadic Effects in F*”. 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

↑ Microsoft Research Inria Joint Centre (неопр.). MSR-INRIA. Дата обращения: 28 мая 2020. Архивировано 21 мая 2020 года.
↑ ¹ ² https://www.fstar-lang.org/#people
↑ Release 0.9.6.0 — 2018.
↑ FStarLang/FStar (неопр.). GitHub. Дата обращения: 28 мая 2020. Архивировано 10 июля 2020 года.

[1] Microsoft Research Inria Joint Centre (неопр.). MSR-INRIA. Дата обращения: 28 мая 2020. Архивировано 21 мая 2020 года.

[_b8508bf1e972c2f3-2] ¹ ² https://www.fstar-lang.org/#people

[_dd736b7166069b47-3] Release 0.9.6.0 — 2018.

[4] FStarLang/FStar (неопр.). GitHub. Дата обращения: 28 мая 2020. Архивировано 10 июля 2020 года.

[4]

[1]

[2]

[3]

F*

Литература

Ссылки

Примечания

Дополнительно по теме

Категории

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