Jonathan Protzenko

Friday blogging: compiling Rust to C (yes) jonathan.protzenko.fr/2025/10/28/e...

Charon: An Analysis Framework for Rust With the explosion in popularity of the Rust programming language, a wealth of tools have recently been developed to analyze, verify, and test Rust programs. Alas, the Rust ecosystem remains relativel...

Yes we would automate the generation of that "thin" layer. We have plenty of existing tooling to do so, we could use e.g. charon arxiv.org/abs/2410.18042 to inspect the function signatures, and generate the wrappers.

If the proposal (forgot where the link is) to guarantee an extern "C" ABI for slices goes through, the wrapper will be greatly simplified.

The plan is to go through the extern "C" ABI for the sake of i) FIPS certification and ii) being able to link against a system version of SymCrypt. This will involve a thin unsafe wrapper that re-exports the original Rust signatures to a Rust client through the C ABI.

This is what I've been driving for the past year! It's an exciting time, with Rust making its way into one of the most critical pieces of software: the core crypto library used in Azure and Windows. With Rust, formal verification becomes easier, and so far, no blockers to Rust adoption.

Friday blogging, about our journey replacing Python's built-in cryptography with verified code from HACL*. I'm very proud of this work: I wrote the first version in 2020, and along the way it had both research (ICFP paper) and industrial impact (Python).

jonathan.protzenko.fr/2025/04/18/p...

Very proud to announce that our original paper on Catala, presented at ICFP'21, received a SIGPLAN Research Highlight. Incredible surprise! Only four papers received this award for the 2021-2023 period. Congratulations @denismerigoux.bsky.social

Boffins carve up C so code can be converted to Rust Mini-C is a subset of C that can be automatically turned to Rust without much fuss Computer scientists affiliated with France's Inria and Microsoft have devised a way to automatically turn a subset of C code into safe Rust code, in an effort to meet…

Boffins carve up C so code can be converted to Rust