I 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 :-)

Correct 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?