Coding 2024-02-02
Question: is Dafny "of the belief" that the ghost version takes on a single value? Because, if so, why isn't the lemma "obvious", and if not, what the heck does any of this mean?
Question: is Dafny "of the belief" that the ghost version takes on a single value? Because, if so, why isn't the lemma "obvious", and if not, what the heck does any of this mean?
Extremely excited to rewrite my tasks.py file to run dafny verify path/to/dfyconfig.toml as much as possible.
Hoarding property definitions like a really weird dragon.
Actually trying to work with some of this rigorously is still a real shock to the system.
I'm not retyping those names.
Cutting edge technology, in that there are many edges to cut oneself on.
I don't intend to inflict these names on anyone else more than this post already does so.
No idea if this will work. Slightly worried it'll drain my battery. Oh well.
Uuuuuugh again
I really hope "if you're missing certain asserts, it just spins its wheels forever" is something that's going to go away.