none of your example problems or solutions use the heap. they all use local (mutable) variables and immutable data structures. I'd argue, that's what makes the (imperative) verification so nice in Dafny. /8
-
-
(and, as an aside, this also means that your solution to fulcrum doesn't have the performance characteristics you claim, since appending a single element to an immutable sequence is O(n)) /9
2 replies 1 retweet 11 likes -
anyway, if you want my best reconstruction of what people mean when they say "FP is easier to reason about", it's that "pure FP doesn't ask me to reason about the heap" /10
1 reply 3 retweets 14 likes -
now, maybe most people who spout "FP is easier to reason about" don't have this in mind; I'm not sure. but I think there's something fundamental about heap vs no heap.
5 replies 2 retweets 4 likes -
you can observe this fundamental distinction inside Dafny, too. try writing some heap manipulating examples (eg, arrays instead of seqs). I think you'll find Dafny scales less well.
2 replies 1 retweet 5 likes -
on solutions to
@Hillelogram's problems? or on using the heap vs not in Dafny?0 replies 0 retweets 1 like -
Aliasing is my guess. Same problem as with goto: it allows spooky action at a distance, which means there's more cases you have to prove correct. If I write Len(arr), I have to prove that arr is unchanged.
0 replies 0 retweets 2 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.