Английская Википедия:F* (programming language)
Шаблон:Short description Шаблон:Distinguish Шаблон:Infobox programming language
F* (pronounced F star) is a functional programming language inspired by ML and aimed at program verification. Its type system includes dependent types, monadic effects, and refinement types. This allows expressing precise specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml, F#, and C for execution. Previous versions of F* could also be translated to JavaScript.
It was introduced in 2011[1][2] and is under active development on GitHub.[3]
History
Versions
Up until version 2022.03.24 F* was written entirely in a common subset of F* and F# and supported bootstrapping in both OCaml and F#. This was dropped beginning in version 2022.04.02.[4][5]
References
Sources
External links
Шаблон:ML programming Шаблон:Microsoft FOSS Шаблон:Microsoft development tools Шаблон:Microsoft Research
- Английская Википедия
- Functional languages
- ML programming language family
- .NET programming languages
- Microsoft programming languages
- Microsoft Research
- Dependently typed languages
- Automated theorem proving
- Programming languages created in 2011
- Proof assistants
- 2011 software
- Страницы, где используется шаблон "Навигационная таблица/Телепорт"
- Страницы с телепортом
- Википедия
- Статья из Википедии
- Статья из Английской Википедии
