Computing Atlas

How Computing Was Built
Sign In
Text size
100%
Theme

Switch Atlas

Programming Language

Dafny

Multi-Paradigm Language

Dafny is an imperative and functional compiled language that compiles to other programming languages such as C#, Java, JavaScript, Go and Python. It was created by K. Rustan M. Leino at Microsoft Research and first appeared in 2009 as a verification-aware language, meaning that verification is required alongside code development. Programmers state preconditions, postconditions, loop invariants and loop variants, and the tool discharges the resulting proof obligations automatically using the Boogie intermediate language and the Z3 theorem prover. It also offers object-oriented features such as generic classes, dynamic allocation and inductive datatypes. It is statically and strongly typed and released under the MIT license.

Facts
Classification
Typing Discipline
Statically Typed 1
Typing Discipline
Strongly Typed 1
First Released
2009 2
Connections

Follows Typing Discipline

Static Typing, Concepts

Entity-backed identity for the typing discipline value this language already carries as an enum fact, resolved to a concept entity by an explicit value-to-entity map (phase 3 bucket conversion, docs\design_entity_backed_browse_buckets_20260928.md). The enum fact itself stays on the entity unchanged.

Strong Typing, Concepts

Entity-backed identity for the typing discipline value this language already carries as an enum fact, resolved to a concept entity by an explicit value-to-entity map (phase 3 bucket conversion, docs\design_entity_backed_browse_buckets_20260928.md). The enum fact itself stays on the entity unchanged.

In Field

Programming Language Theory, Fields
Source Dafny (Wikipedia)

Licensed Under

MIT License, Concepts
Source Dafny (Wikipedia)
Sources
1. Dafny (Wikipedia)
  • Licensed Under: MIT License, Infobox license field
    license = MIT
  • In Field: Programming Language Theory, Lead sentence
    Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go, and Python.
View the Source
2. Wikidata: Dafny
  • Wikidata Q48989398, class allow-list match (w-wdresolver-0926)
  • Wikidata Q48989398 P571 (inception)
View the Source
Comments (0)
No comments yet. Be the first to share a thought.
Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.