# Dafny

24 Hacker News commenters recommended Dafny and 3 criticized it, November 2025 to November 2026. It was recommended in 12 of 13 months. It meets the Hacker Approved badge rule.

**Verdict:** Recommended as a simple, approachable language for proving code correct, with executable output. Critics question its developer experience and production use.

## Why people recommend it

- Simple and approachable to learn (5 comments): "For software projects it seemed very approachable, even for a complete newbie like me." ([source](https://news.ycombinator.com/item?id=49114202)) "Dafny fits that bill quite well, it's simple, it offers refinement types" ([source](https://news.ycombinator.com/item?id=46295905)) "Dafny is really simple. The barrier of entry is low." ([source](https://news.ycombinator.com/item?id=46071763))
- Well designed, efficient verification semantics (3 comments): "Dafny's expressiveness tends to be more in the service of coherent specifications" ([source](https://news.ycombinator.com/item?id=46300707)) "The semantics of Dafny is carefully designed to make verification efficient." ([source](https://news.ycombinator.com/item?id=46297195)) "The language is well designed for this." ([source](https://news.ycombinator.com/item?id=46297285))
- Expressive specifications and invariants (3 comments): "in Dafny one can express much more complicated and complex invariants which get checked at build time" ([source](https://news.ycombinator.com/item?id=46296953)) "Dafny's expressiveness tends to be more in the service of coherent specifications" ([source](https://news.ycombinator.com/item?id=46300707)) "A verification language capable of enforcing invariants" ([source](https://news.ycombinator.com/item?id=46513781))
- Named among serious verification languages (4 comments): "Lean doesn’t have a monopoly on verification languages. Dafney, Rocq, Why3, ATS, Agda, Idris… these all can do it too." ([source](https://news.ycombinator.com/item?id=47244826)) "are definitely worthy of consideration" ([source](https://news.ycombinator.com/item?id=47928558)) "Dafny and F* are two good showcases" ([source](https://news.ycombinator.com/item?id=47104716))

## Alternatives hackers recommend

- [SPARK Ada](https://hackerapproved.com/p/spark.md): 63 recommend
- [Verus](https://hackerapproved.com/p/verus.md): 23 recommend
- [F*](https://hackerapproved.com/p/f.md): 17 recommend

## Cite as

Hacker Approved, "Dafny", https://hackerapproved.com/p/dafny/ (counts from 1,795,640 Hacker News comments, November 2025 to November 2026).