Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Dafny: Verification-Aware Programming Language

dafny.org

Post reply on HN
Print view View original

31–35 of 35 posts

Re: Dafny: Verification-Aware Programming Language

#31

Post by fithisux »

sriku wrote: post #15
sriku wrote: post #14

I quite like Dafny, despite my first run up with it (verification aspect) being frustrating. The language is well designed for this. Also, it looks like it is a great candidate as a code generation target for LLMs because you can generate the proof of correctness and run a feedback loop with Dafny's checker. Try writing a^b in integers and proving its correctness. The simple version works (based on a x a^(b-1)). But…

Am working on rewriting an imperative programming course to use Dafny to present verified algorithms and data structures.

Please post HN when you finish.

Re: Dafny: Verification-Aware Programming Language

#32

Post by rurban »

fooker wrote: post #6

This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?

That's what we use when we can limit our loop count and recursion depth somehow. Prove it for small data, and infer from it for big data.

I use C and C++ model checkers, like cbmc and its variants (esbmc) successfully, but you need to adjust your tests and loops a bit. Like #ifdef __VERIFIER__ or #ifdef __CPROVER__ https://diffblue.github.io/cbmc/cprover-manual/index.html

Re: Dafny: Verification-Aware Programming Language

#33

Post by csb6 »

tgv wrote: post #29

I got a bit into SPARK (a subset Ada of that has formal verification) with AoC, and while it can be tricky, SPARK is quite flexible in how much you prove. Dafny sounds interesting, but I can't find a comparison between the two. There's obviously a difference in memory management, but the rest looks quite similar at first sight, and their niche is quite similar. Does anyone know of a (deeper) comparison between both l…

One difference is that SPARK is intended primarily for safety critical, real-time software (often for embedded systems), while Dafny is meant for teaching purposes and non-real time applications (i.e. environments where a large runtime and garbage collection are permissible). Dafny compiles to C#/Java/Go/etc. and is meant to be interoperable with them so I think it aims at similar use cases as those languages.

Re: Dafny: Verification-Aware Programming Language

#34

Post by fooker »

rurban wrote: post #32
fooker wrote: post #6

This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?

That's what we use when we can limit our loop count and recursion depth somehow. Prove it for small data, and infer from it for big data. I use C and C++ model checkers, like cbmc and its variants (esbmc) successfully, but you need to adjust your tests and loops a bit. Like #ifdef __VERIFIER__ or #ifdef __CPROVER__ https://diffblue.github.io/cbmc/cprover-manual/index.html

There seems to be a bunch of papers and tools that extend CBMC for unbounded loops with k-induction!

Re: Dafny: Verification-Aware Programming Language

#35

Post by fooker »

ashton314 wrote: post #24
fooker wrote: post #19

Earlier quoted context omitted.

Dafny seems to have loops too, and the way it solves the problem you mentioned is forcing the user to write these invariants. I assume if you were to develop such a system for C, C++, or Rust you'd similarly expect the user to do this.

Right. The problem is that those languages are relatively permissive in their type systems. Obviously Rust can capture more in its type system than C can. You would probably want a type like “decreasing unsigned integer” for Rust and some way to enforce monotonic decreasing, which Rust doesn’t give you. (Any experts on formal verification please correct any inaccuracies in what I say here.) The upshot of it is that C…

You are answering a question you want to answer, not the one I asked! :)

Yes, dependent types can encode nice constraints, but so can asserts and assumes.

I am not seeing the fundamental difference in yeeting these constraints to a solver. Dafny seems to do the same thing with Z3.

Post reply on HN