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 …
-
-
...in that I find FP helps me understand a program, but only informally from what the types tell me. And the types help me be productive, but aren't necessarily for guaranteeing correctness beyond some small (but useful) properties.
-
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
- 2 more replies
New conversation -
-
-
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.
-
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.
- 2 more replies
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.