3 ms·

I think humanity in general are only dimly aware of this space. The Research section is probably your best bet about what's different. I think your questions ar

by jfoutz 2y ago

I think humanity in general are only dimly aware of this space. The Research section is probably your best bet about what's different. I think your questions are what academics call "open".

abeppu 2y ago
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