3 ms·
I think PolarSSL showed it can be done with reasonable effort and it is not a suicide.
by sanxiyn 9y ago
I think PolarSSL showed it can be done with reasonable effort and it is not a suicide.
- jabot 9y agoI would really like to see a comparison of the efforts of a) writing a program in a safe language like rust and b) writing the language in C and verifying it with a toolset like the one used by the polarssl guys. Given that the number of C projects that use similar toolsets is... low (?), I'd guess that said comparison would favor rust, but I'm prepared to be surprised :-)
- blub 9y agoCorrect me if I'm wrong, but is this Frama-C and ACSL? That doesn't look like plain C to me. In the ACSL manual in Example 2.10, does the programmer have to add the asserts? What if they make a mistake in the annotation?