Hacker News Reader

Comment by seibelj | Hacker News Reader

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)

View on HN

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!

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

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!

I see. Googled the for Dafny quick sort and it does have some pretty long invariants.

[1]: http://rise4fun.com/Dafny/ks

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".

Yes, you can define predicates that take parameters and use them as the invariants

> much more intuitive than Coq

Is there software that is less intuitive than Coq?

Microsoft Word

Reply on news.ycombinator.com