I think LLM can help here in various ways. For example, by inferring preconditions/postconditions and loop invariants automatically. Also, perhaps, by writing lemmas as required automatically. I'd guess there has been some work on this already, but not sure.
So, you can use fixed-width data types in Dafny and verify properties about functions using them. For example, in our EVM implementation we have types like u8, u16, u256, etc. Of course, Dafny won't let operations on these types underflow or overflow, so it does mean more work ensuring your code doesn't allow this.
Yeah, so as I understand it, AWS is using Dafny generated (Java) code in production. I think we can assume it won't be as efficient has hand written code (at this stage anyway) but it does give you the added guarantees.
> The problem with Dafny and other SMT solvers is that when they work, they're brilliant, but when they don't, they're infuriating
Yeah, look I'm not going to disagree with that. I have had plenty of frustrating times figuring out why something won't verify with Dafny. But, the more you do it, the easier it gets. And, we should work on the assumption that these tools will get better.
> Languages like Coq, Lean, and Isabelle/HOL are better in that you prove things manually (unless you abuse `auto` and tactics for non-trivial proofs, then you still run into the above).
So, it is nice that you always feel like you can make progress with these tools. But, at the same time, that progress can be awfully slow and painstaking. I think the sweet spot lies in using automation as much as possible, but with the fall back option of proving things manually. Dafny to some extent lets you do this, as you can always fall back on manual induction using a lemma.
I agree. There are tools though which are specifically for determining worst-case execution time for e.g. embedded systems which can actually give accurate timing information (upto a point).
Yeah, so these tools will not tell you how long it will take to terminate --- only that it will eventually. In the vast majority of cases, that is what you want to know.
> there are a huge number of useful loops that do useful work and for which you can prove properties like termination
Exactly! If the loop doesn't terminate, then you obviously cannot show it. But if it does, then you should be able to (even if that requires some changes to help the tool)
So, what do you think would be better than "~="? (that's a genuine question since the syntax is not locked down yet by any means). I thought about "isa", also "<:" (following academic papers) and, of course, plain old "instanceof". But, the latter is too much finger typing for me ...
Oh, and of course we could do something like "typeof(x) == int" etc
The good news about undecidability is that, for the most part, it's not a problem. That is, the problem instances that arise in practice are almost never actually undecidable.