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.
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.
14 comments
[ 3.9 ms ] story [ 42.4 ms ] threadand in 2017: https://news.ycombinator.com/item?id=13440324
[0]: https://arxiv.org/abs/1706.04023
Thank you!
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.
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.
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.