I have been delving into Fstar [1] which has an SMT backend and provides a means of program verification. Fstar programs can then be code extracted to OCaml or

I have been delving into Fstar [1] which has an SMT backend and provides a means of program verification. Fstar programs can then be code extracted to OCaml or Fsharp. I think the combination of SAT solving, and a formal language like F* that can create executable OCaml or Fsharp code will be very useful in creating a pragmatic path to verified programs. [1] https://www.fstar-lang.org/ Edit: I wanted to add that I prefer the Lisp syntax of SMT to the python, but that's based upon personal bias. However, a Lisp-like syntax was chosen due to the ease of parsing Lisp s-expressions.