Also known as Fstar, F star, FStar
Язык программирования, основанный на ML
Official website
F*: A Proof-Oriented Programming Language
fstar-lang.org →Link to the official site · 25,395 chars · not written by Vinony
Wikidata facts
- Instance of
- source-to-source compiler
- Official website
- www.fstar-lang.org
Show 8 more facts
- operating system
- cross-platform
- influenced by
- Lean
- copyright license
- Apache Software License 2.0
- programming paradigm
- imperative programming
- source code repository URL
- github.com/FStarLang/FStar
- official blog URL
- fstarlang.github.io
- programmed in
- F#
- software version identifier
- 0.9.6.0
via Wikidata · CC0
Article · Русский
F * (произносится как F star) — функциональный язык программирования, основанный на ML и ориентированный на формальную верификацию разрабатываемых на нём программ. Его система типов включает в себя зависимые типы, монадические эффекты и . Этих выразительных средств достаточно, чтобы задавать точные спецификации для программ, включая описания функциональной корректности и свойств безопасности. Механизм проверки типов в F* позволяет доказывать, что программы соответствуют их спецификациям. Это делается с использованием комбинации SMT-решателя и ручных доказательств. Программы, написанные на F*, могут быть странслированы в OCaml, F# и C для дальнейшей компиляции и выполнения. Предыдущие версии F* также можно было транслировать в JavaScript. Последняя версия F* написана полностью на общем подмножестве F* и F# и может быть запущена как с использованием OCaml, так и с использованием F#. Исходный код языка открыт под лицензией Apache 2.0 и активно разрабатывается на GitHub.
Abstract from DBpedia / Wikipedia · CC BY-SA