>> We have written 20,000 lines of low-level F* code, implementing the TLS 1.3 record layer.
>> HACL*, our High Assurance Crypto Library,
>> (1) We provide HACL∗, a “high-assurance crypto library” implementing and proving

lines of Low∗) several cryptographic algorithms, including the Poly1305 MAC [Bernstein
> Это частное мнение создателей библиотеки.

Это повторный пук в лужу, под видом джакузи.

>> the ICFP 2017 Paper provides an overview of KreMLin as well as a paper formalization of our compilation toolchain
>> We illustrate the design of Low∗ using several examples from our codebase. We show the

ChaCha20 stream cipher [Nir and Langley 2015], focusing on memory safety (§2.1), and the
Poly1305 MAC [Bernstein 2005], focusing on functional correctness. (§2.3). Going beyond functional
> Тоже частное мнение (анотация) к работе.
> Будут цитаты из официальных страниц языка? Или опять гулко треснул?

Зачем ты продолжаешь газифицировать лужи?