7 ms·
What were the things that were confusing? I tried it out and found it much more intuitive than Coq (especially in the proofs). The keywords made sense, and so d
by harpocrates 10y ago
What were the things that were confusing? I tried it out and found it much more intuitive than Coq (especially in the proofs). The keywords made sense, and so did the error messages. That said, I come from a more math oriented background, and I've played typed around with this sort of thing for a while now. So yeah, I'm honestly interested in hearing your perspective!
- seibelj 10y agoFrom what I remember, the assignment was to write a function that implemented quick sort (or something else moderately complex) and getting it to run and satisfy the proof checker was exhausting. Edit: Found a forum post I made during it asking for help. Oh, the frustrating memories... https://dafny.codeplex.com/discussions/546995 https://dafny.codeplex.com/discussions/546995
- pierrec 10y agoWow, the feedback you got on that forum has a pretty rare level of detail and helpfulness. Confusing syntax, perhaps, but the community is point for sure!
- harpocrates 10y agoI see. Googled the for Dafny quick sort and it does have some pretty long invariants. [1]: http://rise4fun.com/Dafny/ks http://rise4fun.com/Dafny/ks
- archgoon 10y agoDoes Dafny not provide any macros for their invariants declarations ensures clauses? The QuickSort Example has a lot of the same invariants again and again, and most of them boil down to "I swear that the integer values are valid indices into the array".
- houli 10y agoYes, you can define predicates that take parameters and use them as the invariants
- skrebbel 10y ago> much more intuitive than Coq Is there software that is less intuitive than Coq?
- nickpeterson 10y agoMicrosoft Word