Content deleted Content added
Jerryobject (talk | contribs) →External links: WP:CATEGORY add. |
Jerryobject (talk | contribs) WP:LINKs add. |
||
Line 25:
}}
'''F*''' (pronounced ''F star'') is a [[High-level programming language|high-level]], [[Comparison of multi-paradigm programming languages|multi-paradigm]], [[Functional programming|functional]] and [[Object-oriented programming|object-oriented]] [[programming language]] inspired by the languages [[ML (programming language)|ML]], [[Caml]], and [[OCaml]], and intended for [[program verification]]. It is a joint project of [[Microsoft Research]], and the [[French Institute for Research in Computer Science and Automation]] (Inria).<ref name="MS-Inria"/> Its [[type system]] includes [[dependent types]], [[Monad (functional programming)|monadic]] [[Side effect (computer science)|effects]], and [[refinement type]]s. 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 [[satisfiability modulo theories]] (SMT) solving and [[Proof assistant|manual proofs]]. For execution, programs written in F* can be translated to [[OCaml]], [[F Sharp (programming language)|F#]], [[C (programming language)|C]], [[WebAssembly]] (via KaRaMeL tool), or [[assembly language]] (via Vale toolchain). Prior F* versions could also be translated to [[JavaScript]].
It was introduced in 2011.<ref name="origin-paper">
| |||