Feature request: Verification succeeded but...

Sep 6, 2011 at 12:42 PM

Here is an idea for a VCC feature. Current VCC output is either "Verification of foo succeeded" or "Verification of baz failed". How about a third option: "Verification of qux succeeded (under 4 assumptions)." This would make it clear to the user whether there is any "cheating" going on in the verification, i.e. whether qux is *really* verified. 

Sep 8, 2011 at 7:35 AM

Hi John,

I suppose we could / should add "grave warnings" on assumptions in the implementation; we have similar warnings for other things... Then the warnings could be counted...

Best, Mark