4 ms·

I'm very much not at the level of accomplishing formal proofs. But isn't his challenge different than what he's trying to prove? I guess my objection is in the

I'm very much not at the level of accomplishing formal proofs. But isn't his challenge different than what he's trying to prove? I guess my objection is in the category of "even if formal proofs aren't easier in FP, it doesn't matter". In particular, when people talk about the advantages of FP and "correctness", they aren't literally talking about formal provability - they're more talking about a spectrum of correctness, that the purely functional approach catches moves more buggy behavior from runtime to compile-time, that the functional implementation is more correct, etc. If you adopt the strict definition of "correct", then "more" correct makes no sense, of course. I recently ported a fairly hairy lengthy algorithm from python to scala. From something with a ton of mutability, scope confusion, exceptions serving as GOTOs for business logic - into scala pure functions. The python was inscrutable with a team of people treating it gingerly. The scala is easily refactorable and each time we take another crack at it, it shrinks into smaller and smaller code (and not by using crazy Scala) and I suspect that much of the confusing hairy complexity will disappear. I don't really know how to quantify this, but I don't think it's captured from an exercise that compares difficulty in formally proving methods in IP and FP. So yeah... it's an awesome exercise that showed a lot, and I really want to dig more into provers, but I just don't see that his "therefore" follows, that "it's (not) easier to reason about FP than imperative".

fusiongyro 9y 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 9y ago
  Haskell 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 9y ago
    Link?
    - pseudonom- 9y ago
      Not 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 9y ago
        No offense, but this is like asking to see an example of someone doing OOP in C and being handed C++.
js8 9y ago
> From something with a ton of mutability, scope confusion, exceptions serving as GOTOs for business logic - into scala pure functions. The python was inscrutable with a team of people treating it gingerly. The scala is easily refactorable and each time we take another crack at it, it shrinks into smaller and smaller code (and not by using crazy Scala) and I suspect that much of the confusing hairy complexity will disappear. I have noticed the same thing with my Haskell code. In other languages with side effects, I often tend to write much more complicated procedures, with cross-cutting concerns. Haskell forces me to break it down more. Maybe FP really is harder to reason about (and write), and that's why people have to write it much more clearly in more manageable chunks. But paradoxically, the net effect is positive, it's actually what makes it easier to reason about (and read) in the end. (And the separation of side effects makes a big difference here.) > I don't really know how to quantify this I was thinking about this. Maybe there should be some information theory framework that could capture complexity of functions (including side-effects). For example, compare how many bits of information enter on input, how many bits are potentially different on output. Then you would have a measure of complexity of individual functions.
bvinc 9y ago
I just wonder if the advantages you're talking about have anything to do with the functional nature of the language or not. Maybe an imperative language with a strong type system and without exceptions would have the same effect? Maybe it's just a general nudging of the language that makes it hard to write bad code? What if you converted the Scala code back to python? Would it have the same good design? And then, even if it's possible to write beautifully designed code in Python, does it even matter if teams consistently end up writing bad code? Yeah, this is a hard thing to quantify and a formal proof challenge doesn't really help.
- lmm 9y ago
  > Maybe an imperative language with a strong type system and without exceptions would have the same effect? In what sense would such a language be imperative? Are you talking about allowing state mutation? I'm pretty sure that would introduce most of the problems the Python had. Functional is not so much a thing as the absence of a thing - an imperative language (i.e. a language in which evaluation order is visible and relevant) essentially consists of a functional language plus one or more unmanaged noncommutative effects. > What if you converted the Scala code back to python? Would it have the same good design? And then, even if it's possible to write beautifully designed code in Python, does it even matter if teams consistently end up writing bad code? Good coding is refactoring, just as good writing is rewriting. If you converted the Scala back to Python it would have its current beautiful design for now, but as you worked on it the design would decay, because it's so much harder to safely refactor imperative and untyped code, so you do less of it, and it becomes harder to see the essence of the code that should be properly factored, in a vicious cycle.

fusiongyro 9y 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 9y ago
Haskell 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 9y ago
  Link?
  - pseudonom- 9y ago
    Not 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 9y ago
      No offense, but this is like asking to see an example of someone doing OOP in C and being handed C++.

js8 9y ago

> From something with a ton of mutability, scope confusion, exceptions serving as GOTOs for business logic - into scala pure functions. The python was inscrutable with a team of people treating it gingerly. The scala is easily refactorable and each time we take another crack at it, it shrinks into smaller and smaller code (and not by using crazy Scala) and I suspect that much of the confusing hairy complexity will disappear. I have noticed the same thing with my Haskell code. In other languages with side effects, I often tend to write much more complicated procedures, with cross-cutting concerns. Haskell forces me to break it down more. Maybe FP really is harder to reason about (and write), and that's why people have to write it much more clearly in more manageable chunks. But paradoxically, the net effect is positive, it's actually what makes it easier to reason about (and read) in the end. (And the separation of side effects makes a big difference here.) > I don't really know how to quantify this I was thinking about this. Maybe there should be some information theory framework that could capture complexity of functions (including side-effects). For example, compare how many bits of information enter on input, how many bits are potentially different on output. Then you would have a measure of complexity of individual functions.

bvinc 9y ago

I just wonder if the advantages you're talking about have anything to do with the functional nature of the language or not. Maybe an imperative language with a strong type system and without exceptions would have the same effect? Maybe it's just a general nudging of the language that makes it hard to write bad code? What if you converted the Scala code back to python? Would it have the same good design? And then, even if it's possible to write beautifully designed code in Python, does it even matter if teams consistently end up writing bad code? Yeah, this is a hard thing to quantify and a formal proof challenge doesn't really help.

lmm 9y ago
> Maybe an imperative language with a strong type system and without exceptions would have the same effect? In what sense would such a language be imperative? Are you talking about allowing state mutation? I'm pretty sure that would introduce most of the problems the Python had. Functional is not so much a thing as the absence of a thing - an imperative language (i.e. a language in which evaluation order is visible and relevant) essentially consists of a functional language plus one or more unmanaged noncommutative effects. > What if you converted the Scala code back to python? Would it have the same good design? And then, even if it's possible to write beautifully designed code in Python, does it even matter if teams consistently end up writing bad code? Good coding is refactoring, just as good writing is rewriting. If you converted the Scala back to Python it would have its current beautiful design for now, but as you worked on it the design would decay, because it's so much harder to safely refactor imperative and untyped code, so you do less of it, and it becomes harder to see the essence of the code that should be properly factored, in a vicious cycle.