redjamjar

Yeah, ok that’s fair enough!!

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.

> I hope this is a typo

Yeah, sorry --- that is a typo.

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.

> The halting problem has almost no practical relevance because we don't really care about the general case.

Yup, agreed

Yeah, SPARK/Ada is a comparable system to Dafny. I agree with that! Also, Frama-C and a bunch of other more esoteric research languages as well.

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.

Haha, yeah ... this one you would have a very hard time with :)

Hopefully, though, termination of your program does not depend on this ... otherwise could be a long wait!

> 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)

Nice job!! Love the 8 ball example ... really fun :)