F*: A Proof-Oriented Programming Language

Introduction F* (pronounced F star) is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving. F* programs compile, by default, to OCaml. Various fragments of F* can also be extracted to F#, to C or

[fcicq]

coq?

[lanius]

"F* is a new higher order, effectful programming language (like ML) designed with program verification in mind".

[theatrical]

Fstarのサイト。すごい雑に言うと、F#ベースのCoqみたいな言語