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 …
-
-
I know there's a lot of excitement about using DP for full proofs, but the main exciting thing for me is being able to push _some_ property tests onto the type system, like matrix multiplication or state machines
-
I think we're a long way from full proofs in DTP being worth the cost. But with some careful language design, maybe we can make some interesting properties provable cheaply. Liquid Haskell is a big step forward here and I want to steal things from it...
- 1 more reply
New conversation -
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.