5 ms·
>One might assume he is using Haskell I am. >and is assuming that because the compiler accepts his code it is therefore correct I am not. >of course this is
by imanaccount247 12y ago
>One might assume he is using Haskell
I am.
>and is assuming that because the compiler accepts his code it is therefore correct
I am not.
>of course this is a fallacy
Just as fallacious as assuming your code is correct because you tested it or ran it.
- cbd1984 12y agoIf correctness can't be demonstrated by mathematical proof, and it can't be demonstrated by comprehensive test suite, how can it be demonstrated? What kind of definition of 'correct' are you using?
- codygman 12y agoPerhaps mathematical proof + comprehensive test suite (including property/fuzz testing) + (time used without bugs showing up * number of people using it)
- jpgvm 12y agoHe never posited that code couldn't be proven correct by formal methods, only that he doesn't assume the type system compiling it makes it correct.
- tel 12y agoHaskell 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 :)
- imanaccount247 12y agoCorrectness can be demonstrated by mathematical proof. But I am using haskell, which does not have a type system powerful enough for that.
- orbifold 12y agoThis does not prevent you from proving the program correct by hand. Regrettably that is rarely done, but could in principle be done regardless of the type system of the language. Of course that would require you to write a specification of the of the features you want to implement, which might be messy depending on your problem domain.
- heinrich5991 12y agoI tried that once at a small piece of code, however the problem was that there was no way to verify the code implemented what the proof said about it.
- imanaccount247 12y agoI'm not sure what this has to do with me. Again, I never said you can't prove programs correct. I simply stated how I work: I don't run my code nearly as often as I would when working in C.