Dafny: verification-aware programming language | Hacker News Reader

Dafny: verification-aware programming language

github.com

78 pointslelf14 comments

Meta: I think the genius of GitHub was showing the README.md, nicely formatted, front-and-center. (I find it baffling that they crop it on mobile, in favor of "Pulse" and "Notifications" and other junk I've never once wanted.) Today even when projects have proper webpages, we link to the GitHub page, because the README has more/better/easier-to-digest information.

The Dafny webpage at microsoft.com appears to have some formatting errors (perhaps auto-converted from some other format, with no proofreading), and I can't tell if it's been updated at all in the past 10 years.

Similarly, I think Wikipedia and StackOverflow are much more likely than the average webpage to be able to provide me the information I want, with no fuss. HN is the most usable forum, followed by (old) Reddit.

As developers and designers, we say we want more features and flexibility. As users, we eschew any webpages that use this flexibility. We just want plain webpages with information. Webpages which are a trivial pretty-printing of some plain text (wiki/markdown) are by far my favorites.

And the files. Other VCS UIs show other things first. I don't care about commits or branches first. I care about the README and the top-level files (e.g., LICENSE).

If you are a contributor your priorities might shift, but there are probably ways to handle that.

I suspect the real problem is trying to use the same landing page for both an intro and a project management tool. Create two pages and tune them accordingly.

I am a contributor to many repos.

Good answer to "What's the difference between LEAN, F* and Dafny?" https://stackoverflow.com/questions/46010923/whats-the-diffe...

Excellent comment as the first thing I thought after seeing the submission was exactly "how does it compare to f* and lean"?

Thank you!

Discussed in 2016: https://news.ycombinator.com/item?id=10842714

and in 2017: https://news.ycombinator.com/item?id=13440324

What is up with that logo?

I kind of like it, looks like a beach

Can I specify a regular expression as an argument to a string type or demand an integer or a real argument to be a solution of a certain equation with this? Can it also handle validation of certain data against other data in runtime (e.g. load a list of available options from a database and make sure no value that is not in that list gets is allowed as a parameter to a certain function)?

It's backed by z3, an SMT solver. There are theories in SMT for strings that can sometimes answer questions of your first flavor, but I don't know if they're in z3.

Solvers can also answer questions of your second variety, but again, sometimes they can't, and they can't be guaranteed to in general. For an example, consider this example: https://rise4fun.com/Dafny/Cube where the "ensures" on the return value enforces exactly that.

You also should be able to write set-inclusion style queries like your second clause, i.e. a function that takes an element and a list of elements as an input and only returns true if the element is contained within the list of elements. I think? I'm not sure why you couldn't.

Of course, whether or not that does what you think it does or not depends on how something can get written to that database - if there was a path to write something new to your exclusion list from elsewhere in your application, then the "verified" code would return true when you would think it would return false but it was doing exactly what you told it to do. Is this a problem with your design, or the verification? I'd argue the design, but verification-nihilists would probably say it's a problem with the verification.

I see. Thanks.

I have become interested in Dafny after reading about how they are making an effort to reduce annotations[0].

[0]: https://arxiv.org/abs/1706.04023

What does it have for a standard library?

Reply on news.ycombinator.com