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

11–20 of 35 posts

Re: Dafny: Verification-Aware Programming Language

#11

Post by porcoda »

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?

Not a stupid question at all. There are two reasons verification tends to happen in these specialized languages: the languages we usually use are often not expressive enough to write things like specifications, and a bit too expressive in the sense of letting people write program logic that is insanely difficult to verify (think untyped pointers into a dynamically allocated heap for example). So these verification related languages often are more expressive on the spec side and more restrictive in terms of what kind of code you can write.

Re: Dafny: Verification-Aware Programming Language

#12

Post by nextos »

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?

The semantics of Dafny is carefully designed to make verification efficient.

Dafny can compile to and interface with a few languages, including C#.

Re: Dafny: Verification-Aware Programming Language

#13

Post by algorithmsRcool »

fjfaase wrote: post #3

Looks interesting. I saw some C# files, from which it seems it is implemented in C#. Is there going to be an implementation in Dafny?

It could be done, but what would be the virtue of it? Most programming languages are not self-hoisted for a reason.

Re: Dafny: Verification-Aware Programming Language

#14

Post by sriku »

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 if you write an "optimised one" using (with handwaved details) (a^(b/2))^2 .... pulled some serious hair trying to prove this function works.

Re: Dafny: Verification-Aware Programming Language

#15

Post by sriku »

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.

Re: Dafny: Verification-Aware Programming Language

#17

Post by mikiskk »

This formal verification course I took by Manos Kapritsos and Jon Howell is taught in Dafny and assumes no former experience with the subject. Most of the exercises are to some degree “self-grading” as proof success means you have a correct solution, provided your spec is correct. I highly recommend.

https://glados-michigan.github.io/verification-class/fall202...

Re: Dafny: Verification-Aware Programming Language

#18

Post by fooker »

nextos wrote: post #12
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?

The semantics of Dafny is carefully designed to make verification efficient. Dafny can compile to and interface with a few languages, including C#.

What does it mean for verification to be efficient?

Are there benchmarks showing dafny is faster than other inefficient options ?

Re: Dafny: Verification-Aware Programming Language

#19

Post by fooker »

ashton314 wrote: post #10
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?

> … verify/synthesize invariants in languages people use? Good question. This is the holy grail. This is what everyone in PL research would love. This is where we want to get to. Turns out a language as “simple” as C has sufficiently complicated semantics as to limit rigorous analysis to the basics. One example is loop analysis: it’s very useful to know that a loop will terminate eventually; if a loop is modifying so…

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.

Re: Dafny: Verification-Aware Programming Language

#20

Post by fooker »

quamserena wrote: post #8
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?

Most existing mainstream languages aren’t expressive enough to encode these invariants. For languages outside of the mainstream, Lean 4 is a language supporting verification, and it’s also a full programming language, so you can write your proofs/theorems in the same language that you program in.

What's an invariant you can not encode in a general purpose programming language?

I'd have assumed, by virtue of being Turing complete, you could express any invariant in almost any language?

Post reply on HN