[jacquesm]

It serves as a reminder that even though this implementation has been proven correct that does not rule out bugs in the proof or in the method used to create the proof.

[gsnedders]

Or that your compiler produces code equivalent to the (proven) correct C.