This is pretty cool. The tutorial opens up in a web page with frames and an fstar editor. You can follow along with the tutorial by reading the steps in one panel and trying it out in another panel without needing to download fstar. There are 15 steps each with substeps, and the tutorial will remember where you were after you close the page. I won't just regurgitate their exercises here of course as there would be no point - you can do the tutorial for yourself, and regurgitating would neither add anything "new" to the web about fstar, nor "summarize" existing info about fstar, which serves the purpose of saving you time, allowing you to go to the main source for a more detailed understanding. For now I will just give a non-exhaustive quickie-summary of things I learned in step 1 :

  1. Knowing OCaml, F#, Standard ML, or Haskell is helpful in learning fstar
  2. An Emacs extension exists for fstar
  3. F* doesn't actually execute code - it just verifies it. To create code you must use either an OCaml or F# compiler

Next I will continue through step 1.1.

Girl Reading a Book image
Image by delo from Pixabay