I think this is a fair challenge. I verified left-pad in Agda; it isn't very pretty: https://gist.github.com/rntz/aaaaf7a0bdb1cc65c49adb6adde29728 … Admittedly, I don't think Agda is aimed at this kind of problem. Anyone who's up to date on verification for FP languages want to take a shot at it?https://twitter.com/Hillelogram/status/987432178840756225 …
-
-
Replying to @arntzenius
Hillel Retweeted Ranjit Jhala
Yeah, we got a few!
@stevecheckoway did it in pure Dafny (https://rise4fun.com/Dafny/RF6L ),@RanjitJhala did it in LiquidHaskell (https://twitter.com/RanjitJhala/status/987728366189985792 …), and apparently@edwinbrady wrote a version for Idris that's part of the stdlib.Hillel added,
3 replies 0 retweets 4 likes -
Replying to @hillelogram @arntzenius and
Oh, did I? I was thinking it would be possible to set things up to do this neatly, but honestly I think your basic position is reasonable...
2 replies 0 retweets 3 likes -
Replying to @edwinbrady @arntzenius and
One of the fascinating things about this challenge is that none of big "FP > IP" advocates wrote successful proofs, while AFAICT all of the people who wrote successful proofs hold similar positions to mine: maybe prefer one in general, but which is "better" is contextual.
2 replies 0 retweets 3 likes -
Replying to @hillelogram @edwinbrady and
Like I generally find it easier to think in state machines and contracts, but there's still plenty of problems where I'd find it much easier to think in function composition. I try to be excited about everything.
1 reply 0 retweets 1 like
I find reasoning about state much easier in functional languages, curiously enough... It's almost as if this is a hard problem with no good answer yet! Being excited about everything seems the right approach :).
-
-
Replying to @edwinbrady @arntzenius and
And almost like different people think of systems differently :D
0 replies 0 retweets 1 likeThanks. Twitter will use this to make your timeline better. UndoUndo
-
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.