Stop showing the number of verified procedures when Dafny finishes

[keyboardDrummer]

Stop showing the number of verified procedures when Dafny finishes verification. This number refers to Boogie procedures, which are an implementation detail not visible to Dafny users, and therefor doesn't carry much meaning.

I think could consider changing the message of nothing was verified (easy), and we could consider showing how many Dafny symbols were verified (harder) (symbols such as newtypes, subset types, iterators, functions, methods, constants with subset types, datatype constructors with default arguments).

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[davidcok]

Though the actual number 'verified' may not be meaningful, it does provide value (to me) indicating
a) a result of 0 things are verified (with no errors), if unexpected, is a quick warning that the command-line is not what was intended
b) the overall magnitude also gives some indication of the amount of work being done.

Perhaps the presence of --verbose can provide more information?

[MikaelMayer]

I would not like to delete this number which does convey intuition as @davidcok says.
If we followed your reasoning till the end, we should also remove the number of errors because it is also similarly an internal detail as in this example:

function method Fib(i: nat): (r: int)
  decreases i
  requires i > 1
  requires Fib(i-1) > 0
  ensures r > 0
{
  -1
}

it contains only one declaration, yet Dafny says

Dafny program verifier finished with 0 verified, 2 errors

The reason for that is that both the well-formedness and the function's verification condition have errors.
By the way, even if we did not have Boogie, we would still need to verify the well-formedness and the function's verification condition, so it's not a Boogie internal detail, it's a Dafny internal detail, which makes more sense to show. Boogie does not know the difference between well-formedness and verification condition for Dafny's purposes.

Disclaimer: I am not using the CLI at all myself, so I would recommend seeking the advice of something using it for the first time as well as advanced users.

Other debatable ways we could improve this summary:

• As @davidcok suggested, replace the result with "Dafny verified everything" and "Dafny could not verify everything", and the --verbose option could tell more about how many of these were verified
• A percentage of verification. Percentages don't need to disclose the sets.
• A grouping of the counts so that we only report top-level declaration counts, so my example would say "1 declaration with errors" instead of "2 errors"

[keyboardDrummer]

If we followed your reasoning till the end, we should also remove the number of errors because it is also similarly an internal detail as in this example

I like that train of thought, but doesn't the number of reported errors directly correspond to the number of errors we list in the CLI ?

I think more explicitly the current message would be "Dafny program verifier finished with X hidden things verified, and Y errors shown under this message"

By the way, even if we did not have Boogie, we would still need to verify the well-formedness and the function's verification condition, so it's not a Boogie internal detail, it's a Dafny internal detail, which makes more sense to show.

Whether you group the WFness and the contract in a single SMT program, or as separate ones, is an implementation detail right? You could also split further and split the WFness check into several SMT programs.

[MikaelMayer]

If we followed your reasoning till the end, we should also remove the number of errors because it is also similarly an internal detail as in this example

I like that train of thought, but doesn't the number of reported errors directly correspond to the number of errors we list in the CLI ?

Oh that CLI is worse than I thought! Good call. You're right. This discrepancy is slightly misleading.
However, I am big proponent of having positive feedback to give a sense of the work Dafny did, so that we are not under-selling Dafny as well. Could you please replace the number of "procedures" by the number of assertions that were sent to Dafny?
In either case, I think that it's better to have positive feedback, so removing it is worse that having one that is slightly misleading.

I think more explicitly the current message would be "Dafny program verifier finished with X hidden things verified, and Y errors shown under this message"

Yes, something like that, instead of "hidden things" you could say something more user-friendly like "X declarations or specifications verified"

By the way, even if we did not have Boogie, we would still need to verify the well-formedness and the function's verification condition, so it's not a Boogie internal detail, it's a Dafny internal detail, which makes more sense to show.

Whether you group the WFness and the contract in a single SMT program, or as separate ones, is an implementation detail right? You could also split further and split the WFness check into several SMT programs.

I agree that it would be better t show things that users can relate rather than internal details. So if we replaced "X verified" by "X assertions verified" or at least "X declarations" where we merge well-formedness of specifications and the implementation, I would be more pleased than "X declarations or specifications verified".

[MikaelMayer]

Fun fact, in previous versions of the Dafny VSCode plugin, we were showing the following:

I'm not sure we want to reuse the term "proof obligation", but we could reuse "assertion batch".