Actually it does look like their book has at least some additional info in their intro section "To F*, or not to F*?" The highlights seem to be: - extensional

Actually it does look like their book has at least some additional info in their intro section "To F*, or not to F*?" The highlights seem to be: - extensional equality (similar to nuprl) - undecidable type-checking - combination of both SMT and tactics, metaprogramming - focus on compilation to mainstream languages, programming more than formalizing math