First of all, I didn't mean my FUD remark to be vitriolic.

I disagree that it is more work in total; I don't think you're taking into account the work that will no longer have to be done, namely work spent searching for cross-module bugs introduced when a security proof for one module relies on a condition which cannot be expressed in the underlying language.

I agree that it is a new type of work though.

Edit: easier for the mathematician who wants to prove that system X has security characteristic Y