Proof-oriented Programming in F*

19 points by nextos

osa1

For a PL verification task (e.g. type system soundness) how do I choose betweek: Rocq, Lean, F*, ...?

I know what to look for in a PL, but I last time I did verification was a decade ago and I'd just picked Coq at the time as it had the resources (Software Foundations), and I have no idea what to look for in a proof assistant to use for PL verification.

amw-zero

Rocq is by far the most popular at the moment. Lean is very promising for the future, with its backing by a big corporation and adoption by some high profile people like Terrence Tao.

I really like the design of F* though. It seems focused on verification of practical programs, and I am a sucker for any ML language.
- nextos
  
  I really like the design of F* though. It seems focused on verification of practical programs
  
  Exactly. IMHO, Dafny, Why3, and F* are excellent for verification of practical programs. They don't get the attention they deserve.
juuso

Anecdotal experience; Agda (and its extensions like Cubical Agda) seems to be the one people research type systems in. I estimate that most people don't have a principled approach to choosing a theorem prover -- you pick your horse and maybe down the line you understand your problem is better solved in another system for a reason you wouldn't have understood initially.
julesjacobs

General choice: Lean

Separation Logic: Rocq+Iris

Type theory research: Agda

Embedded low level programming: F*

Realistically, start with Lean
toastal

We left ATS, Why3, & Dafney out of the list?

rtpg

val max (x:int) (y:int) : int
let max x y = if x >= y then x else y

val max1 (x:int) (y:int)
  : z:int{ z >= x && z >= y && (z = x || z = y)}
let max1 x y = if x >= y then x else y

let max2 (x:int) (y:int)
  : z:int{ z = max x y }
  = if x > y
    then x
    else y

^ these refinement types are very neat.

It is a bit hard to deal with "SMT couldn't solve this"-style errors... would kinda hope that at least for simple stuff it would be able to spit out a counterexample in those cases. I wonder if it would be easy to wire up the SMT solver to go the other direction in those scenarios and attempt the counterexample

ahelwer

I think that is how SMT usually works. For checking some formula F, negate F and then check to see whether it is satisfiable (aka, find the counterexample). If !F is satisfiable, that means F is invalid. If !F is not satisfiable, that means F is valid.

nextos

Also available as PDF, for those interested:

https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf