My goal is to try to prove each solution correct, using appropriate types.
To run the solutions, you will need to replace the include in each Makefile with your own installed Makefile.include from the F* distribution.
F* is an OCaml-like language for "proof-oriented programming". It supports:
- dependent types and proofs
- a metaprogramming system
- reasoning about effectful programs
Wiki: https://github.com/FStarLang/FStar/wiki
Old tutorial: https://fstar-lang.org/tutorial/tutorial.html
Incomplete new tutorial: https://www.fstar-lang.org/tutorial/
My guide to using tactics, in this repository: "Tactics for the complete noob"
Language features I didn't find in the tutorials, an ongoing list
There's a Slack instance but it requires a google.com or microsoft.com email address to sign up.
The "fstar-club" mailing list site hasn't responded when I've tried to visit it.
I've joined the Zulip forum for F*, but it appears to be low-traffic: https://fstar.zulipchat.com/
The precompiled Linux binaries need a newish version of glibc. Ubuntu LTS 18.04 didn't work, I upgraded to Ubuntu LTS 20.04 (glibc 2.31) and that seemed OK. Then I started puzzling out the dependencies for the "hello world" example.
I found that batteries doesn't work with 4.13. Try version 4.12. (Unfortunately there wasn't a clear error message that this was the problem; opam does a complicated process to match dependencies, and does not seem to have an error for "your compiler is newer than this package supports."
In the INSTALL guide for F*, it says:
Note: To compile OCaml code generated by F*, using a F* binary package is not the preferred method. You should install F* via OPAM instead.
This was not mentioned in https://github.com/FStarLang/FStar/wiki/Executing-F%2A-code, alas. So this is what I ended up doing; install opam, use it to install OCaml 4.12, and then installed F*