Meaningful value for "Dafny program verifier finished with 1 verified, 0 errors"

[keyboardDrummer]

What numbers is Dafny referring to when it says "Dafny program verifier finished with 1 verified, 0 errors" ?

Currently the first number refers to Boogie implementations, which has no meaning to Dafny users. The second number is the amount of assertions that Dafny failed to verify.

We can change this to:

• Report the number of Dafny symbols, functions, methods, datatypes, constants, etc, that were verified.
• Report the number of assertions, explicit or implicit, that were verified.

I vote we report the second, the number of assertions. This high granularity in the number means users get better feedback when using options that filter which assertions are actually verified. Also, it makes the first and the second number look at the same type of thing: assertions.

[robin-aws]

Couldn't agree more that the current metric is pretty meaningless, and that the number of Dafny-level assertions would be better.

I also suggest, though, that it would be better to not output this by default at all, since the number is almost never useful information. This would let the dafny CLI align with the Silence is Golden philosophy. See also #3460 and #3213.

The only time I can see it being useful is as a sanity check: if 0 assertions were in scope to verify but you didn't expect that. But I think a better solution there is a warning if there was nothing to verify, similar to the warning we already emit if no code is in scope at all.

[atomb]

I agree with both of you. Defaulting to no output is nice, and reporting on Dafny-level assertions when we say anything also seems better. I would like it to be easy to get output equivalent to what we get right now (but in terms of assertions) but I think it makes sense for it to be off by default.

[MikaelMayer]

there is a warning if there was nothing to verify, similar to the warning we already emit if no code is in scope at all.

I wouldn't put a warning if there is nothing to verify. Nothing to verify could indicate that the code is simple (e.g. Hello World), putting a warning for our first-time users would be a wrong experience.

Between symbols and assertions, there are assertion batches as well, and outside of both, files, but I'm not sure I want either of them.

I'm against the idea of no output by default, but I'm in favor of changing the existing output if it makes sense. If the user says "dafny verify x.dfy" and the result of this is exit code 0 and nothing printed, it feels like Dafny did not do any work. There are so many assertions in single declarations that it would not make that much sense to add the numbers of all the assertions of every declarations. I'd be rather in favor of saying how many declarations were verified, how many had errors. This corresponds nicely to error contexts in the IDE and also the side-bar when turning verification as tests.

[keyboardDrummer]

I wouldn't put a warning if there is nothing to verify. Nothing to verify could indicate that the code is simple (e.g. Hello World), putting a warning for our first-time users would be a wrong experience.

I think so too, but I think we could make an exception for the dafny verify command, since it implies the user is expecting to verify something.

I'm against the idea of no output by default

👍 Having output by default seems safer to me, and biasing for safety seems good in the Dafny context.

There are so many assertions in single declarations that it would not make that much sense to add the numbers of all the assertions of every declarations.

There are a lot, so many that you won't be able to recognize the number from your code, but I do think seeing how this number changes between CLI invocations allows you to get a better feeling of what Dafny is doing.

For example, when you add a single statement that adds a single provable implicit assertion, you'll see the effect in the CLI output, so you can learn that Dafny has implicit assertions. Another example is that you'll see the difference between and empty method with no ensures clause, which proves 0 assertions, and one that does have something to prove.

Secondly, when you're using the --filter-position option, which can cause Dafny to only verify a single assertion, or even zero assertions if you specify a line that has no assertion, then a method will only be partially verified, and knowing the absolute number of proven assertions is critical. We could show the number of proven assertions only when this option is used, but I don't like having an exception for that, and I think there is general educational value in showing the number of assertions.

I'd be rather in favor of saying how many declarations were verified, how many had errors. This corresponds nicely to error contexts in the IDE and also the side-bar when turning verification as tests.

I expect to add an IDE feature that changes the granularity of what is verifiable, from methods to assertions, so you can, when using --isolate-assertions, see play icons for each assertion in the gutter.

@MikaelMayer are you OK with reporting Dafny level assertions? Robin and Aaron are on board, but I'd like full consensus before I update the many .expect files ^,^