Исходное сообщение
"Новая криптографическая библиотека EverCrypt с математически..." Отправлено Аноним84701, 07-Апр-19 17:35
> )))) пройдите по ссылке указанной выше, и вовсе не компиляция, а трансляция (кодогенерация) Выше по ссылке 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", поэтому прискипывание к конечной формулировке (тем более, после перевода) вряд ли что-то даст в конечном результате (т.е. вне опеннета).

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:	>> )))) пройдите по ссылке указанной выше, и вовсе не компиляция, а трансляция (кодогенерация) > Выше по ссылке > 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", поэтому прискипывание к конечной формулировке (тем более, после перевода) > вряд ли что-то даст в конечном результате (т.е. вне опеннета).
	Введите код, изображенный на картинке: