> It seems likely then that verification only works on the subset of > expressiveness that can be cowritten in the free and the constrained > language. i.e. we aren't verifying c at all.
Isn't this a direct consequence of C being Turing-complete and therefore not verifiable in the general case? That is, we know C gives you more than enough rope to hang yourself with and therefore we want to encourage people to use C in ways that are explicitly verifiable. To me, you've concisely summed up exactly what (I think) LangSec is all about! pete _______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
