Dafny Alternatives
Similar projects and alternatives to dafny
-
-
-
Scout APM
Less time debugging, more time building. Scout APM allows you to find and fix performance issues with no hassle. Now with error monitoring and external services monitoring, Scout is a developer's best friend when it comes to application development.
-
-
Rust-for-Linux
Adding support for the Rust language to the Linux kernel. (by Rust-for-Linux)
-
checkedc
Checked C is an extension to C that lets programmers write C code that is guaranteed by the compiler to be type-safe. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors. Checked C does not address use-after-free errors. This repo has a wiki for Checked C, sample code, the specification, and test code.
-
interactive
.NET Interactive takes the power of .NET and embeds it into your interactive experiences. Share code, explore data, write, and learn across your apps in ways you couldn't before.
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
SonarQube
Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.
-
rust
Rust for the xtensa architecture. Built in targets for the ESP32 and ESP8266 (by esp-rs)
-
tlaplus
TLC is an explicit state model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
-
-
Pandas
Flexible and powerful data analysis / manipulation library for Python, providing labeled data structures similar to R data.frame objects, statistical functions, and much more
-
-
-
mintable
🍃 Automate your personal finances – for free, with no ads, and no data collection.
-
-
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
-
-
dafny reviews and mentions
- Automated Reasoning at Amazon: A Conversation
-
There is framework for everything.
Most verification languages will do this. There are many of them but for something relatively easy to pick up, look at Dafny: https://github.com/dafny-lang/dafny
-
Six programming languages I’d like to see
Ada is already mentioned here.
You also want to look at Dafny for a contract-based language: https://github.com/dafny-lang/dafny
Since it has verification support it also covers the second point about semantic relations.
-
Make formal verification and provably correct software practical and mainstream
It is still alive, it has just moved to github! It is a big language and it can prove useful programs. Apparently, part of the Ethereum 2 specification was verified using it. https://github.com/dafny-lang/dafny
-
Value tagging?
This isn't really true. For example, there's Dafny which uses Z3 to discharge SMT proofs, LiquidHaskell which uses Z3 to discharge SMT proofs, F* which uses Z3 to discharge SMT proofs, combined with human-authored proofs.
-
A list of new budding programming languages and their interesting features?
Dafny: A modern imperative proof language.
-
How does the Dafny Programming Language compile-time check its constraints?
I was just pointed to Dafny, a formally verified imperative programming language. A few example snippets from their introductory paper are:
-
What would an implementation of runtime type checks in a dependent type context look like?
Check out Dafny
-
Soundness
As you can see it is fully functional and only creates a finite (and small) number of objects. This code is public, since it was posted to the Dafny bug tracker I'm currently writing some articles about it. trait BadTrait{function method contradiction():()ensures false} class BadClass{ const tr: BadTrait constructor(tr: BadTrait) { this.tr := tr; } } class T { const f: T -> BadClass constructor(f: T -> BadClass) { this.f := f; } } function method app(x: T): BadClass { x.f(x) } method Main() { var x := new T(app); ghost var \_ := app(x).tr.contradiction(); assert false; print "false is true!"; // actually prints! } As you can see, Ghost+termination_bug = soundness_bug
-
ISO C became unusable for operating systems development
You're right that you can't define a safe subset of C without making it practical. MISRA C defines a C subset intended to help avoid C's footguns, but it still isn't actually a safe language. There are alternative approaches though:
1. Compile a safe language to C (whether a new language or an existing one)
2. Formal analysis of C, or of some practical subset of C, to prove the absence of undefined behaviour
Work has been done on both approaches.
ZZ compiles to C. [0] Dafny can compile to C++, but it seems that's not its primary target. [1][2]
There are several projects on formal analysis of C. [3][4][5][6]
[0] https://github.com/zetzit/zz
[1] https://github.com/dafny-lang/dafny
[2] https://dafny-lang.github.io/dafny/
[4] https://www.microsoft.com/en-us/research/project/vcc-a-verif...
-
Foundations of Dawn: The Untyped Concatenative Calculus
Formal methods have been used successfully for decades; it's not just a pipe dream. Perfect software should ideally be something like ultra-low-defect software, though (that's the term the AdaCore folks use).
There are also other projects that aim to make formal software development much easier [0][1] and of course there's SPARK Ada.
-
What I wish I knew when learning F#
It's also important to add F# is an inspiration for an amazing MS Research effort, F* [1].
Furthermore, it is also worth checking Dafny [2] (Spec#'s successor). The relationship between Dafny and C# is equivalent to the relationship between F* and F#. Both languages try to refine their predecessors semantics and augment them with practical constructs to prove program correctness.
Some of the largest software artifacts ever verified have been implemented in Dafny [3].
[1] https://www.fstar-lang.org
[2] https://dafny-lang.github.io/dafny/
[3] https://www.cs.columbia.edu/~junfeng/17sp-e6121/papers/ironf...
- How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors
- Linux Rust Support
-
Large-Scale Programming & Testing & ProLang
I'm unsure if you'll remember Dafny (https://github.com/dafny-lang/dafny) from PSoft, but that's what your message sounds like. I knew exactly what my Dafny code had to do, it made sense in my head, but the syntax was whack-- and the documentation was worse.
Stats
dafny-lang/dafny is an open source project licensed under GNU General Public License v3.0 or later which is an OSI approved license.
Popular Comparisons
Are you hiring? Post a new remote job listing for free.