Not saying it isn´t useful but with this change Python's crypto depends on Microsoft (https://fstar-lang.org/ and https://project-everest.github.io/)
Not saying it isn´t useful but with this change Python's crypto depends on Microsoft (https://fstar-lang.org/ and https://project-everest.github.io/)
> HACL* is a formally verified library of modern cryptographic algorithms, where each primitive is verified for memory safety, functional correctness, and secret independence. HACL* provides efficient, readable, standalone C code for each algorithm that can be easily integrated into any C project.
> All the code in this repository is released under an Apache 2.0 license. The generated C code from HACL* is also released under an MIT license.
You have an unusual definition of "depends on Microsoft". Anyone worried about depending on Microsoft should be able to maintain 15k lines of C that are already formally verified. Python already vendored the code so who cares who wrote that code?
[flagged]