I guess it's a bit popular right now

    * Error 17 at Welcome.fst(24,0-28,30):
      - Could not start SMT solver process.
      - Command: ‘/home/site/wwwroot/fstar/bin/z3’
      - Exception:
          Unix.Unix_error(Unix.ENOENT, "create_process", "/home/site/wwwroot/fstar/bin/z3")
    
    1 error was reported (see above)

> https://fstar-lang.org/tutorial/

FYI: The link to this tutorial is unluckily a little bit obscured on the F* website: Go to

> https://fstar-lang.org/index.html#learn (1)

and click on the image below the text "You probably want to read it while trying out examples and exercises in your browser by clicking the image below.".

In the section of (1) also the PDF version is linked:

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...