News for hackers. Stuff that matters.

A comment on Jonathan Blow on Rust. Parent comment

Re:Jonathan Blow on Rust by ausimian on Sunday February 02, 2020 @08:28PM (#22220734)
VCC[1] was a substantial piece of research from MSR aimed at supporting the verification of C (not C++) via a theorem prover. However, it appears in a study[2] of its application to parts of the Hyper-V code-base, there were some practical difficulties relating to proving performance in the developer workflow.

Still, fascinating to see work like this on real-world code-bases with established languages. You can also see very similar work in languages like Dafny[3].

[1] https://github.com/microsoft/vcc [2] http://moskal.me/pdf/tphol2009.pdf [3] https://github.com/dafny-lang/dafny

[ Parent | on HN ]
Re:Jonathan Blow on Rust by mmoskal on Monday February 03, 2020 @01:23PM (#22227205)
There are also efforts at ETH to verify Rust using SMT solvers using methods similar to VCC and Dafny, see https://www.pm.inf.ethz.ch/research/prusti.html

Adding verification once you have code is generally more difficult, though in case of VCC it was helpful to have a large example code base to make sure the tool would cover the major patterns, especially relating to concurrency primitives.

[ Parent | on HN ]