What does HackerNews think of dafny?
Dafny is a verification-aware programming language
C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.
The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].
[1] https://www.microsoft.com/en-us/research/project/code-contra...
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
The language (Dafny): https://github.com/dafny-lang/dafny
Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Go, Python, Java, or JavaScript (more to come!), so it can integrate with your existing workflow.
I really agree with this. The situation is a bit crazy. Since formal proofs are hard, the alternative taken is giving no guarantees at all. That's bad. Static analyzers can get really far. Contracts, even just at runtime are really useful. I don't want a piece of code to run if the precondition is not met, and I don't want it to return or have side effects if the postcondition is not met. This would rule out a massive class of errors. Of course, bonus points if you can do it at compile time.
Ada SPARK, Infer [1] and Dafny [2] show that rigorous engineering is possible and practical. Actually, Facebook (Meta now) argues Infer let's them move faster.
I think the problem is political and economical. It's hard to monetize this first. I wish someone like Apple took the plunge and rebuilt a simpler version of their stack using formal verification. It's the kind of thing only a large corporation or a government can do because it might take half a decade to take off. Once it takes off its unstoppable. Who would not like to buy e.g. a phone where most bugs and security breaches are impossible by construction? Verification also has a nice side effect. Change for the sake of change and featuritis are pretty incompatible with it.
Are the mechanisms for defining architectural styles and some predefined styles (OO call/return, pipes & filters, REST and event broadcast) all that is new from Objective-S? Any other future goals? These seem relatively easy to implement as e.g. Lisp macros? Clojure supports many of these.
Personally, I would like to see more research in program semantics. I think languages should try to reduce expressiveness whenever possible by offering mechanisms to do so, i.e. DSLs and DSL tools. Along with the total lack of popularity of design-by-contract / Hoare logic / refinement types, I think this is the biggest mistake in modern language design.
In other fields, engineers strive to use components and to combine them in ways that yield artifacts with provable properties. An elementary example of this are truss structures in mechanical engineering.
There is not that much research direction in this area. Personally, I like Dafny [2]. There is quite a lot of research on advanced type systems and theorem proving, but I think there is still a big gap in usability and automation. I think DSLs to restrict semantics + automated program analyses could be an excellent alternative. Infer [3] is pretty nice. Similar approaches that targeted a language with better semantics would be able to offer a lot more guarantees.
--------------
[1] https://aws.amazon.com/blogs/security/protect-sensitive-data... [2] https://github.com/dafny-lang/dafny
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.
I have been learning it and the syntax is close to most C style programming languages. As a software developer this makes it much more approachable than Coq. The proof statements also feel more like the math I learned in college rather than the weird magic keywords of Coq.
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...
There are also other projects that aim to make formal software development much easier [0][1] and of course there's SPARK Ada.
Dafny Cheat Sheet: https://docs.google.com/document/d/1kz5_yqzhrEyXII96eCF1YoHZ...
Looks like there's a Haskell-to-Dafny converter.
[0]: https://www.fstar-lang.org
[1]: https://www.microsoft.com/en-us/research/project/checked-c/
[2]: https://www.microsoft.com/en-us/research/project/vcc-a-verif...
[3]: https://github.com/koka-lang/koka
[4]: https://github.com/dafny-lang/dafny
[5]: https://www.microsoft.com/en-us/research/project/project-ver...
I don't think anyone is suggesting it will be. It's not about to supplant Ada SPARK, for instance, as Rust is far behind in terms of formal analysis.
> just like what the parent pointed out about Java and it's memory safety promises back in the day
Java does address the memory-safety issues of C and C++. You can't have a buffer overflow vulnerability in pure Java code. You can't have any kind of undefined behaviour due to memory-management mistakes in your code. You can't double-free, or use-after-free, or deference a pointer to a local variable that has gone out of scope. You can't trigger undefined behaviour through a read-before-write bug in your code.
It's possible to have a memory leak in Java, if you retain references to objects for too long, but that won't ever give rise to undefined behaviour.
Of course, there can still be bugs in a JVM, but that's another matter. All languages are vulnerable to compiler bugs.
Other languages like JavaScript do the same. It's possible to leak memory, but it's never possible to trigger undefined behaviour from JavaScript. That's a vital part of its security model.
> It is indeed quite possible to write memory safe C/C++ code... and it's done every day
That doesn't sound right.
There's a reason I gave the examples of the Linux kernel and Chromium. They're written by highly competent developers, but they still have subtle memory-management bugs. Most C/C++ codebases are written by less competent developers, but are of far less interest to attackers, so it's of less consequence. Their memory-management bugs are likely to go unnoticed forever.
I agree it's possible to write C/C++ code without memory-management bugs (there are various formal development systems for C), but it's a significant challenge. I'd hope avionics software, for instance, would be entirely free of such bugs.
> You never hear about how memory safe and performant all that code is... you only ever hear about the rare, high profile mistakes.
They're not that rare, they're a major source of serious security vulnerabilities, and languages like Safe Rust can close the door on them entirely.
> The problems with languages like C++ are more about how bloated it's become. There's 30 ways to do anything in that language, and 24 of them you're not supposed to use anymore!
Agreed. C++ is quite a lumbering monster of complexity. Ada also has a reputation for being somewhat bloated, but it's not as far gone as C++.
> if not for memory safety promises, then for it being a "fresh start" for systems programming without all the legacy baggage C++ has
Keep an eye on Zig, too. Also D and Nim, and perhaps Vala. Also the lesser-known ZZ and Dafny languages, which look very interesting.
https://github.com/dafny-lang/dafny
Dafny is not on the list of notable programming languages.
Still, fascinating to see work like this on real-world code-bases with established languages. You can also see very similar work in languages like Dafny[3].
[1] https://github.com/microsoft/vcc [2] http://moskal.me/pdf/tphol2009.pdf [3] https://github.com/dafny-lang/dafny
It's simple enough to be attempted with a limited knowledge of Dafny, but subtle enough that you will need to think about what you are doing