4 ms·
> A huge investment. If you are going to do that then you might as well just move to Rust. People say that, but the people who say this rarely have any practic
by nanolith 2y ago
> A huge investment. If you are going to do that then you might as well just move to Rust.
People say that, but the people who say this rarely have any practical experience using CBMC. It's very straight-forward to use. I could teach a developer to use it reliably, on practical software, in a month.
- pdimitar 2y agoI am not denying it, nor am I claiming that "just move to Rust" is an universal escape hatch. What I am saying is that if it were as simple as "just learn CBMC" then maybe Microsoft and Google would have not published their studies demonstrating that 60% - 75% of all CVEs are memory safety errors like buffer under-/over-flows.
- nanolith 2y agoThese studies aren't wrong. But, that's also because neither Microsoft nor Google make use of practical formal methods in practice. Both have research teams and pie-in-the-sky projects, not dissimilar to this DARPA project. But, when it comes down to the nitty-gritty development cycle, both companies use decades old software development practices.