F* - an ML-like functional programming language aimed at program verification

Stumbled upon F* lang, while going through details about zen-protocol. Having found it somewhat similar to Michelson Lang, thought to share it with the community, in hope, it may inspire, some technical discussion.

F* Lang is a Microsoft research project, in association with INRIA. According to its own introduction …

F* (pronounced F star) is an ML-like functional programming language aimed at program verification. (…) The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml, F#, or C for execution.

1 Like

Nice find. Perhaps a .NET implementation of tezos could be written in this, analogous to NBitcoin for bitcoin.

Interestingly, F* can be translated to OCaml too!

Got to admit sometimes I wonder why does the world need more programming languages.

One idea would be to convert from a subset of FStar to Michelson. It should be very easy to check at least simple invariants that way. Related, during a hackathon, FStar team made an experiment using Solidity and EVM: https://www.cs.umd.edu/~aseem/solidetherplas.pdf

Here’s a blockchain that uses it.

Zen Protocol