5 ms·

Dafny: verification-aware programming language

78 points by lelf 8y ago

dang 8y ago
Discussed in 2016: https://news.ycombinator.com/item?id=10842714 https://news.ycombinator.com/item?id=10842714 and in 2017: https://news.ycombinator.com/item?id=13440324 https://news.ycombinator.com/item?id=13440324
kuwze 8y ago
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 https://arxiv.org/abs/1706.04023
bluetonium 8y ago
Good answer to "What's the difference between LEAN, F* and Dafny?" https://stackoverflow.com/questions/46010923/whats-the-difference-between-lean-f-and-dafny https://stackoverflow.com/questions/46010923/whats-the-diffe...
- Boulth 8y ago
  Excellent comment as the first thing I thought after seeing the submission was exactly "how does it compare to f* and lean"? Thank you!
qwerty456127 8y ago
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)?
- munin 8y ago
  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 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.
  - qwerty456127 8y ago
    I see. Thanks.
ken 8y ago
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.
- cryptonector 8y ago
  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).
  - hinkley 8y ago
    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.
    - cryptonector 8y ago
      I am a contributor to many repos.
ravenstine 8y ago
What is up with that logo?
- camgunz 8y ago
  I kind of like it, looks like a beach
mcguire 8y ago
What does it have for a standard library?

78 points by lelf 8y ago

dang 8y ago

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

kuwze 8y ago

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 https://arxiv.org/abs/1706.04023

bluetonium 8y ago

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

Boulth 8y ago
Excellent comment as the first thing I thought after seeing the submission was exactly "how does it compare to f* and lean"? Thank you!

qwerty456127 8y ago

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)?

munin 8y ago
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 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.
- qwerty456127 8y ago
  I see. Thanks.

ken 8y ago

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.

cryptonector 8y ago
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).
- hinkley 8y ago
  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.
  - cryptonector 8y ago
    I am a contributor to many repos.

ravenstine 8y ago

What is up with that logo?

camgunz 8y ago
I kind of like it, looks like a beach

mcguire 8y ago

What does it have for a standard library?