4 ms·
> If you adopt the strict definition of "correct", then "more" correct makes no sense, of course. On the other hand, it's pretty easy to widen the scope of wha
by fusiongyro 8y ago
> If you adopt the strict definition of "correct", then "more" correct makes no sense, of course.
On the other hand, it's pretty easy to widen the scope of what you're proving correct about a program in such a way as to make it impossible for Haskell to help you. For instance, "accomplish this in O(n)" or "use less than 1 MB" or "in less than 1 second." People usually only concern themselves with the aspects of the implementation that Haskell prioritizes by surfacing as return values. But there are certainly settings where the method used is as important as getting the answer mathematically correct--in fact the rise of NoSQL shows us that there are even situations where doing the wrong thing quickly is better than aborting in the face of unrecoverable errors.
- thesz 8y agoHaskell can help you with "O(n)", "less than 1MB" and many other constraints of that sort. You should use domain-specific language embedded into it for that. If you do that that way, Haskell can help you with particular details of the implementation with types (I think that O(n) would be easy - I did parametrization on the length circa 2008) and help you to connect your implementation and the rest of program, again, with types. I did exactly that. From well-typed parsers for stream processing hardware to (not-so-well typed for historical reasons) strict realtime algorithms.
- fusiongyro 8y agoLink?
- pseudonom- 8y agoNot sure what GP is thinking of, but here's an example of embedding tools for reasoning about performance in Idris: https://www.youtube.com/watch?v=4i7KrG1Afbk&feature=youtu.be&t=1254 https://www.youtube.com/watch?v=4i7KrG1Afbk&feature=youtu.be...
- fusiongyro 8y agoNo offense, but this is like asking to see an example of someone doing OOP in C and being handed C++.