I think NVidia's adoption of SPARK for security critical firmware is victory, sp... | Hacker News

Hacker News new | past | comments | ask | show | jobs | submit

login

pjmlp on Feb 5, 2020 | parent | context | favorite | on: ZZ is a modern formally provable dialect of C

I think NVidia's adoption of SPARK for security critical firmware is victory, specially since they also evaluated Frama-C and Rust as part of their selection process.

Rust probably would have made it in the future, but it is still not mature enough to the domains NVidia intends to use SPARK on.

https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-auto...

MaxBarraclough on Feb 8, 2020 [–]

Rust isn't aiming for formal verification, is it?

steveklabnik on Feb 8, 2020 | [–]

It’s something we’d like and are vaguely pursuing but not at the expense of other things.

MaxBarraclough on Feb 9, 2020 | | [–]

Neat, thanks.

steveklabnik on Feb 9, 2020 | | [–]

No problem. “Rust Belt” and “Miri” are the terms to search for if you want to learn more.

Consider applying for YC's Spring batch! Applications are open till Feb 11.
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact