6 ms·

I had to use this for an algorithms class while getting my CS master's. Very, very tough to use for anything beyond simple experiments. It has confusing syntax

by seibelj 10y ago

I had to use this for an algorithms class while getting my CS master's. Very, very tough to use for anything beyond simple experiments. It has confusing syntax and incomplete documentation. But when you finally get your program to execute, you can be sure it's perfect! (Supposedly)

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 ago
  From 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 ago
    Wow, 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 ago
    I 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 ago
      Does 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 ago
        Yes, 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 ago
    Microsoft Word

by seibelj 10y ago

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 ago
From 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 ago
  Wow, 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 ago
  I 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 ago
    Does 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 ago
      Yes, 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 ago
  Microsoft Word