Dafny: Verification-Aware Programming Language • Hacker News Board

Re: Dafny: Verification-Aware Programming Language

#21

Post by fooker » Wed, Dec 17, 2025, 3:47 AM UTC

porcoda wrote: post #11

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 re…

Yeah I can see pointer weirdness being an issue.

As for being not expressive enough for specifications, isn't the code itself a form of specification? :)

Re: Dafny: Verification-Aware Programming Language

#22

Post by hatefulmoron » Wed, Dec 17, 2025, 4:25 AM UTC

fooker wrote: post #18

nextos wrote: post #12

Earlier quoted context omitted.

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 ?

Dafny and similar languages use SMT; their semantics need to be such that you're giving enough information for your proof to verify in sufficient time, otherwise you'll be waiting for a very long time or your proof is basically undecidable.

I'm not sure about benchmarks comparing languages, but Dafny goes through a lot of tweaking to make the process faster.

Re: Dafny: Verification-Aware Programming Language

#23

Post by esafak » Wed, Dec 17, 2025, 4:37 AM UTC

gz09 wrote: post #4

dionian wrote: post #2

Reminds me of Eiffel, in a good way. Looks awesome. Is there anything close to this in Scala by chance?

It's similar in spirit, but in Dafny one can express much more complicated and complex invariants which get checked at build time -- compared to eiffel where pre/post conditions are checked at runtime (in dev builds mostly).

This expressiveness is a curious point, because a common charge leveled against Scala is that it is too expressive.

Re: Dafny: Verification-Aware Programming Language

#24

Post by ashton314 » Wed, Dec 17, 2025, 5:25 AM UTC

fooker wrote: post #19

ashton314 wrote: post #10

Earlier quoted context omitted.

> … 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.

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, C++, and Rust permit too much behavior that isn’t capturable in the type system. Thus, the properties that you’re interested in are semantic (as opposed to syntactic; type systems turn semantic properties into syntactic ones) so Rice’s theorem applies and there’s no computable way to do the analysis right.

Re: Dafny: Verification-Aware Programming Language

#25

Post by cake-rusk » Wed, Dec 17, 2025, 5:37 AM UTC

fooker wrote: post #21

porcoda wrote: post #11

Earlier quoted context omitted.

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 re…

Yeah I can see pointer weirdness being an issue. As for being not expressive enough for specifications, isn't the code itself a form of specification? :)

Yes, but the quality of the spec varies. For example many (most?) C programs have undefined behaviors which means the spec is incomplete and unreliable. Dafny gives you better tools to avoid this. So in the end you get a higher quality spec with Dafny.

Re: Dafny: Verification-Aware Programming Language

#26

Post by skybrian » Wed, Dec 17, 2025, 7:19 AM UTC

This looks pretty neat, but the mapping to other languages looks rather awkward for string types (for example).

Fine for teaching, but it doesn't seem to be a suitable tool to generate idiomatic library code?

Re: Dafny: Verification-Aware Programming Language

#27

Post by wavemode » Wed, Dec 17, 2025, 7:50 AM UTC

fooker wrote: post #20

quamserena wrote: post #8

Earlier quoted context omitted.

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?

In most languages you can express any invariant, sure, but you can't prove that the invariant is upheld unless you run the program.

For example a NonNegativeInteger type in most languages would just have a constructor that raises an exception if provided with a negative number. But in languages with proofs, the compiler can prevent you from constructing values of this type at all unless you have a corresponding proof that the value can't be negative (for example, the value is a result of squaring a real number).

Re: Dafny: Verification-Aware Programming Language

#28

Post by fjfaase » Wed, Dec 17, 2025, 10:51 AM UTC

algorithmsRcool wrote: post #13

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.

Yes, the primary reason being the bootstrapping problem. But because Dafny can already can generate C# code, that should not be a major problem. It also allows for a gradual conversion where more and more parts are generated from Dagny sources.

I know that maintaining a compiler in its own language poses some problems when you want to extend that language with additional features.

Because compilers are rather complex problems, they can be viewed as a testing stone for a language.

I think it would be nice to have a formally verified compiler. That is a bit more than proving that the sources are correct. But because formally verified compilers are rare, it could promote the usages of Dayne.

I am aware that it would be quite an effort to make it self-hosted and even more to formally verify it correctness.

Re: Dafny: Verification-Aware Programming Language

#29

Post by tgv » Wed, Dec 17, 2025, 11:00 AM UTC

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 languages?

Re: Dafny: Verification-Aware Programming Language

#30

Post by steego » Wed, Dec 17, 2025, 11:19 AM UTC

esafak wrote: post #23

gz09 wrote: post #4

Earlier quoted context omitted.

It's similar in spirit, but in Dafny one can express much more complicated and complex invariants which get checked at build time -- compared to eiffel where pre/post conditions are checked at runtime (in dev builds mostly).

This expressiveness is a curious point, because a common charge leveled against Scala is that it is too expressive.

Expressiveness tends to become a liability when the benefits of the expressiveness aren’t clear.

Dafny’s expressiveness tends to be more in the service of coherent specifications and less in the service of language abstraction for its own sake.