hacspec can be compiled F*. Other formal languages should follow.
The base for the F* compiler is an AST generated from the hacspec. This also allows us to perform rigorous (type) checking on specs.
Run
make
to build the spec checker.
hacspec compiles to F*. Run
make
to build the F* compiler.
The following targets exist for the compiler to generate F* and check specs
from ../specs.
make -C fstar-compiler/specs
make -C fstar-compiler/specs check
make -C fstar-compiler/specs tests
Note that this requires HACL_HOME to point to a copy of HACL* and FSTAR_HOME to a copy of F*.