Jonathan Protzenko
@protz.bsky.social
I talk about Rust, verification, cryptography, programming languages… and pets
Friday blogging: compiling Rust to C (yes) jonathan.protzenko.fr/2025/10/28/e...
Eurydice: a Rust to C compiler (yes)
Perhaps the greatest surprise of the last two years was, for me, the realization that people not only care about compiling C to Rust (for obvious reasons, such as, ahem, memory safety) – they also car...
jonathan.protzenko.fr
October 31, 2025 at 5:09 PM
Friday blogging: compiling Rust to C (yes) jonathan.protzenko.fr/2025/10/28/e...
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.
We're rewriting parts of Microsoft's SymCrypt cryptographic library in Rust to improve memory safety and defend against side-channel attacks, enabling formal verification while maintaining backward compatibility via a Rust-to-C compiler: msft.it/6011SU7Fc
June 10, 2025 at 5:29 PM
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...
jonathan.protzenko.fr/2025/04/18/p...
15,000 lines of verified cryptography now in Python
In November 2022, I opened issue 99108 on Python’s GitHub repository, arguing that after a recent CVE in its implementation of SHA3, Python should embrace verified code for all of its hash-related inf...
jonathan.protzenko.fr
April 18, 2025 at 5:39 PM
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...
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
February 24, 2025 at 10:00 PM
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
Reposted by Jonathan Protzenko
Boffins carve up C so code can be converted to Rust
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…
dlvr.it
January 3, 2025 at 12:35 PM
Boffins carve up C so code can be converted to Rust