iiinova — where your digital self keeps evolving

Jonathan Protzenko

@protz.bsky.social

129 followers 65 following 7 posts

I talk about Rust, verification, cryptography, programming languages… and pets

Posts Replies Media

Jonathan Protzenko @protz.bsky.social · 31/10/2025

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

jonathan.protzenko.fr

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...

031

Jonathan Protzenko @protz.bsky.social · 10/06/2025

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.

66514

Jonathan Protzenko @protz.bsky.social · 18/04/2025

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

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...

041

Jonathan Protzenko @protz.bsky.social · 24/02/2025

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

2154

Reposted by Jonathan Protzenko

The Register @theregister.com · 03/01/2025

Boffins carve up C so code can be converted to Rust

dlvr.it

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…

1135