News for hackers. Stuff that matters.

A comment on Prossimo – Memory safety for the Internet's most critical infrastructure. Parent comment

Re:Prossimo – Memory safety for the Internet's most critical... by howinteresting on Monday June 21, 2021 @10:06AM (#27579281)
The formal verification researchers I've worked with love Rust, because its type system nails the basics so they can focus on proving more interesting properties.

Rust and formal verification work really well together. You can formally verify properties in a small section of critical code, then use the type and lifetime systems to expand those properties to the whole codebase. It's not an either/or, it's a both/and.

[ Parent | on HN ]
Re:Prossimo – Memory safety for the Internet's most critical... by grumblenum on Tuesday June 22, 2021 @07:57AM (#27590571)
That's fascinating. Can you direct me to any of their papers or public work formally verifying a rust codebase? I haven't seen that before.
[ Parent | on HN ]