Jan :rust: :ferris: on Nostr: Compiling C to Safe Rust, Formalized https://arxiv.org/abs/2412.15042 "We apply our ...
Compiling C to Safe Rust, Formalized
https://arxiv.org/abs/2412.15042
"We apply our methodology to existing formally verified C codebases: the HACL* cryptographic library, [...] and show that the subset of #C we support is sufficient to translate both applications to safe #Rust.[...] Of particular note, the application of our approach to HACL* results in a 80,000 line verified cryptographic library, written in pure #RustLang, that implements all modern algorithms - the first of its kind."
Holy cow!🤯
https://arxiv.org/abs/2412.15042
"We apply our methodology to existing formally verified C codebases: the HACL* cryptographic library, [...] and show that the subset of #C we support is sufficient to translate both applications to safe #Rust.[...] Of particular note, the application of our approach to HACL* results in a 80,000 line verified cryptographic library, written in pure #RustLang, that implements all modern algorithms - the first of its kind."
Holy cow!🤯