Context: we have a research project building a "verification debugger" that tries to show exactly this!

How do programmers think about correctness typically, though? They write assertions showing what they think is true. The best feedback on a flawed assertion is to show what is actually known--the gap between what is true and the assertion the user wrote is the explanation.

Yes, exactly.

But why do you say it produces a bigger space of options? That's not obvious to me at all. In fact I think with symbolic execution the space can be smaller because you can focus on verifying one path at a time.

The alternative is to have the verifier show you what it needs to prove at each program point. But this is likely more complicated (it mixes different paths) and less natural. So for debugging (and we are trying to build a proof debugger) we think forward is clearly better.

Ok, but what if a tool like Dafny is supporting your proof and the tool says no? Our hypothesis is that what you want to know (as the user) is what the verifier knows at each program point. Then you compare what it knows to what you expect it should know. That requires forward reasoning.

Yes, I noticed that too, I'd like to understand why!

Also check out the whole Programming Language Pragmatics playlist: tinyurl.com/PLP5vids

And as always, there's more details in the book! amzn.to/4kuKSY2 (Amazon affiliate link)

PLP 8.5.4: Garbage Collection - youtu.be/wfWlgYhvPWI

Also check out the whole Programming Language Pragmatics playlist: tinyurl.com/PLP5vids

And as always, there's more details in the book! amzn.to/4kuKSY2 (Amazon affiliate link)

Maybe it depends on how bad the presentation is ;-) I am not suggesting presentations need to be perfect. But, it would be great if they are understandable by the median audience member and communicate the main idea of the paper effectively.

Also check out the whole Programming Language Pragmatics playlist: tinyurl.com/PLP5vids

And as always, there's more details in the book! amzn.to/4kuKSY2 (Amazon affiliate link)

PLP 8.5 part 2: Recursive Types - youtu.be/TaHerOEKVFo

Also check out the whole Programming Language Pragmatics playlist: tinyurl.com/PLP5vids

And as always, there's more details in the book! amzn.to/4kuKSY2 (Amazon affiliate link)

LOL! But that brings us outside the original question; you can't redirect to /dev/null if it doesn't exist.

No, if no-one can observe a side effect, it doesn't exist!