Content deleted Content added
m Reverted edits by 116.26.109.66 (talk) (HG) (3.4.7) |
No edit summary |
||
Line 21:
}}
'''F*ck''' (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 (computing)#Refinement types|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 [[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]].
| |||