[bolognafairy]

What part of how this is being conveyed do you disagree with? Specifically.

This isn’t a language war.

[neuroelectron]

The headline makes it sound like it was written in Python which is a lot more readable than 15,000 lines of C

[frumplestlatz]

The 15k lines of C are generated. The implementations are written in (and formally verified using) F*, and then the C is generated from the F* code using KaRaMeL.

One should be able to trust the proofs of correctness and never look at (or maintain) the generated C directly.

- https://fstar-lang.org

- https://github.com/FStarLang/karamel

- https://github.com/hacl-star/hacl-star