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
Here we go: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Data/BoundedList.idr … I don't think it proves the full spec (that the first few characters are the padding character), but it shouldn't be too hard to extend.
1 reply 0 retweets 0 likes -
Replying to @hillelogram @arntzenius and
I think it’s only tracking lengths.
1 reply 0 retweets 1 like -
Replying to @RanjitJhala @arntzenius and
Yeah, looks like. I'm suuuuuuuuuper rusty on my Idris but I think you could elegantly handle this by making a homogenous-value-list type. I'd have to futz around a bunch.
1 reply 0 retweets 0 likes
I would like to have a go at this, but I'm currently grading a big pile of Java coursework. Actually that's the perfect excuse to do it isn't it... not that this is really the sort of thing Idris is strong at, but that's not a reason to avoid having a go.
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.