> )))) пройдите по ссылке указанной выше, и вовсе не компиляция, а трансляция (кодогенерация)

Выше по ссылке
https://github.com/project-everest/hacl-star
> All our code is written and verified in F* and then compiled to C via the KreMLin tool.

Еще используется "extraction"
> HACL* relies on F* (stable branch) and KreMLin (stable branch) for verification, extraction to OCaml (specs/) and extraction to C (code/).

https://github.com/FStarLang/kremlin/
> KreMLin is a tool that extracts an F* program to readable C code.
> This work has been formalized on paper. We state that the compilation of such F* programs to C preserves semantics. We start from Low*, a subset of F*, and relate its semantics to CompCert's Clight.

Очевидно, что авторы не пользуются терминологией с явно выраженным различием между "translation" и "compilation", поэтому прискипывание к конечной формулировке (тем более, после перевода) вряд ли что-то даст в конечном результате (т.е. вне опеннета).