Hacker News Reader

Comment by abeppu | Hacker News Reader

As someone only dimly aware of this space, I wish upfront they would highlight what they see as their relative strengths to similar systems and techniques. For example, I'm aware that both NuPRL and Coq have some ability to extract programs from proofs. What kinds of problems does F* do better at? Are there some areas where the SMT solver is a particular advantage? Are the extracted programs superior in some way?

View on HN

F* has an extraction backend which targets "human-readable C" code, contrarily to Coq which extracts proof to "machine-written OCaml" (typically the extracted code use a type-system-escape-hatch left in OCaml for the sake of Coq extraction). Consequently, part of the Everest project (the proven cryptographic primitives in particular) has been integrated into C code base like the linux kernel, firefox .

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".

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

Reply on news.ycombinator.com