KreMlin: from (a subset of) F* to C

Great find, pjmlp! The F star code is incredibly readable. I know nothing about the language but I'm fairly sure I get what it's doing. The difference between it and the C illustrates why it's better to get above C if one can for verification and maintenance. The difference is usually much, much worse. The second, impressive thing is that the C was so close in readability to the F star code.

An interesting project for academics might be re-coding parts of MirageOS's TLS in F star to run through Kremlin. They already wrap C versions of the algorithms IIRC. One could start with the algorithms as a practice run. Then the stateful parts as that's where a lot of risk will be. Then the functional parts. Then integration into a C library.

I cannot express how much I like this. This is a great tool and the right one to write a replacement TLS stack with. Excited for things to come.