5 ms·
Haskell is not quite sufficient to connect mathematical proof to your code. Coq/Agda/Idris are much closer to this idea though and, if you can create a spec in
by tel 12y ago
Haskell is not quite sufficient to connect mathematical proof to your code. Coq/Agda/Idris are much closer to this idea though and, if you can create a spec in one of those systems then a proof really is sufficient.
- dllthomas 12y agoAssuming that spec can genuinely embody everything you care about, about the code. Is this currently possible for performance metrics, anywhere?
- lmm 12y agoYou can express "this code performs at most n primitive steps from this list". Theoretically it should be possible to express any performance requirement in that form, but I doubt it's practical to do for e.g. numeric computation. (It's usable for "no page render require more than 4 db roundtrips" or similar though).
- tel 12y agoI'd bet you could ensure that some kind of tolerance and stability checks were performed and then carry the results around. Ultimately whenever computation relies on dynamic input it's necessary to have a hard-coded "tolerance failure" check. Theoretically you could embed enough analysis in there to have theories about the actual code you're running, too, but I don't think as many analysts care about theorem proving—they're more of an algebraicist's toy.
- tel 12y agoYeah, absolutely. I said "if" rather carefully, ha.
- dllthomas 12y agoThat you did. I certainly didn't mean it as a takedown! I just saw it a subtlety worth stressing, and about which I was eager to learn more if there was more to learn :)