Content deleted Content added
Added a reference in the lead section and updated some categories. |
No edit summary |
||
Line 23:
}}
'''F*''' (pronounced ''F star'') is a [[functional programming language]] inspired by [[ML (programming language)|ML]] and aimed at [[program verification]]. 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]].
Programs written in F* can be translated to [[OCaml]], [[F Sharp (programming language)|F#]], and [[C (programming language)|C]] for execution. Previous versions of F* could also be translated to [[JavaScript]].
| |||