F* (язык программирования)

Ф*
	Официальный логотип Fstar
Парадигма	Мультипарадигмальность : функциональная , императивная.
Семья	ML : Caml : OCaml
Разработано	Нихил Свами, Хуан Чен, Седрик Фурне, Пьер-Ив Струб, Картикеян Бхаргаван, Жан Ян
Разработчики	Исследования Майкрософт , ; Инрия
Впервые появился	2011 год ; 13 лет назад
Стабильная версия	v2023.09.03 / 3 сентября 2023 г .; 10 месяцев назад
Дисциплина набора текста	зависимый , предполагаемый , статичный , сильный
Язык реализации	Ф*
ТЫ	Кроссплатформенность : Linux , macOS , Windows.
Лицензия	Апач 2.0
Расширения имен файлов	.fst
Веб-сайт	fstar-lang .org
Под влиянием
	Coq , Dafny , F# , Lean , OCaml , Standard ML

F* (произносится как F star ) — высокоуровневый , многопарадигмальный , функциональный и объектно-ориентированный язык программирования, созданный на основе языков ML , Caml и OCaml и предназначенный для проверки программ . Это совместный проект Microsoft Research и Французского института исследований в области компьютерных наук и автоматизации (Inria). ^[1] Его система типов включает зависимые типы , монадические эффекты и уточняющие типы . Это позволяет выражать точные характеристики программ, включая функциональную корректность и свойства безопасности. Средство проверки типов F* направлено на то, чтобы доказать, что программы соответствуют их спецификациям, используя комбинацию решения по модулю выполнимости (SMT) и ручных доказательств . Для выполнения программы, написанные на F*, могут быть переведены на OCaml , F# , C , WebAssembly (с помощью инструмента KaRaMeL) или на язык ассемблера (с помощью цепочки инструментов Vale). Предыдущие версии F* также можно было перевести на JavaScript .

Он был представлен в 2011 году. ^[3]^[4] и находится в активной разработке на GitHub . ^[2]

История

Версии

До версии 2022.03.24 F* был полностью написан на общем подмножестве F* и F# и поддерживал загрузку как в OCaml , так и в F#. Начиная с версии 2022.04.02 это было исключено. ^[5]^[6]

Обзор

Операторы

F* поддерживает распространенные арифметические операторы, такие как +, -, *, и /. Кроме того, F* поддерживает операторы отношения, такие как <, <=, ==, !=, >, и >=. ^[7]

Типы данных

примитивов Общие типы данных в F*: bool, int, float, char, и unit. ^[7]

Ссылки

^ Jump up to: ^а ^б «Объединенный центр Microsoft Research Inria» . МСР-ИНРИА .
^ Jump up to: ^а ^б «ФСтарЛанг/ФСтар» . Гитхаб . Проверено 23 апреля 2024 г.
^ Свами, Нихил; Чен, Хуан; Фурне, Седрик; Струб, Пьер-Ив; Бхаргаван, Картикеян; Ян, Жан (сентябрь 2011 г.). Безопасное распределенное программирование с использованием типов, зависящих от значений . ICFP '11: Материалы 16-й Международной конференции ACM SIGPLAN по функциональному программированию. Том. 46. Токио, Япония: Ассоциация вычислительной техники. стр. 266–278. дои : 10.1145/2034574.2034811 . Проверено 17 апреля 2023 г.
^ «Проект F*» . Майкрософт . Проверено 20 апреля 2023 г.
^ «fstar.exe больше нельзя собирать на F# как исполняемый файл .NET #2512» . Гитхаб . Проверено 17 апреля 2023 г.
^ «Рассмотрите возможность отмены требования о том, что код F* должен быть действительным F# #1737» . Гитхаб . Проверено 17 апреля 2023 г.
^ Jump up to: ^а ^б Свами, Нихил; Мартинес, Гвидо; Растоги, Асим (14 января 2024 г.). Доказательство-ориентированное программирование на F* (PDF) .

Источники

Ахман, Дэнел; Хрицку, Кэтэлин; Майяр, Кенджи; Мартинес, Гвидо; Плоткин, Гордон; Проценко, Джонатан; Растоги, Асим; Свами, Нихил (2017). «Монады Дейкстры бесплатно» . 44-й симпозиум ACM SIGPLAN-SIGACT по принципам языков программирования .
Свами, Нихил; Хрицку, Кэтэлин; Келлер, Шанталь; Растоги, Асим; Делинья-Лаво, Антуан; Форест, Саймон; Бхаргаван, Картикеян; Фурне, Седрик; Струб, Пьер-Ив; Кольвайс, Маркульф; Зинзиндоу, Жан-Карим; Занелла-Бегелен, Сантьяго (2016). «Зависимые типы и мультимонадические эффекты в F*» . 43-й симпозиум ACM SIGPLAN-SIGACT по принципам языков программирования .
Свами, Нихил; Мартинес, Гвидо; Растоги, Асим (2024). Доказательное программирование на F* .

Внешние ссылки

Эта языкам программирования, статья, посвященная является незавершенной . Вы можете помочь Википедии, расширив ее .

[MS-Inria-1] Jump up to: ^а ^б «Объединенный центр Microsoft Research Inria» . МСР-ИНРИА .

[GitHubCode-2] Jump up to: ^а ^б «ФСтарЛанг/ФСтар» . Гитхаб . Проверено 23 апреля 2024 г.

[origin-paper-3] Свами, Нихил; Чен, Хуан; Фурне, Седрик; Струб, Пьер-Ив; Бхаргаван, Картикеян; Ян, Жан (сентябрь 2011 г.). Безопасное распределенное программирование с использованием типов, зависящих от значений . ICFP '11: Материалы 16-й Международной конференции ACM SIGPLAN по функциональному программированию. Том. 46. Токио, Япония: Ассоциация вычислительной техники. стр. 266–278. дои : 10.1145/2034574.2034811 . Проверено 17 апреля 2023 г.

[4] «Проект F*» . Майкрософт . Проверено 20 апреля 2023 г.

[5] «fstar.exe больше нельзя собирать на F# как исполняемый файл .NET #2512» . Гитхаб . Проверено 17 апреля 2023 г.

[6] «Рассмотрите возможность отмены требования о том, что код F* должен быть действительным F# #1737» . Гитхаб . Проверено 17 апреля 2023 г.

[:0-7] Jump up to: ^а ^б Свами, Нихил; Мартинес, Гвидо; Растоги, Асим (14 января 2024 г.). Доказательство-ориентированное программирование на F* (PDF) .

[1]

[2]

[3]

[4]

[5]

[6]

[7]