3 ms·

GOTO, mutations, and side-effects break referential equality and equational reasoning, making it much harder to prove things about your program. I guess you can

by sink 11y ago

GOTO, mutations, and side-effects break referential equality and equational reasoning, making it much harder to prove things about your program. I guess you can do that by endless permutations of tests or a stochastic testing system, but that sounds like a horrible way to spend your time.

mden 11y ago
"[They] break referential equality and equational reasoning" Please explain? Mutations can cause side-effects but don't have to. You seem to think that limiting program behavior _necessarily_ alleviates informal reasoning, but that's not the case. Your argument is also highly hyperbolic in terms of testing. A properly designed system with immutability needs to be tested no less than properly designed system with mutability.
- sink 11y ago
  Sure! Mutations ARE side effects. Consider two situations with a function and a mutable variable: First: Your function depends on a value that can mutate. Now you have a hidden parameter to your function. You have to test the function under all reasonable conditions by which the value can change. The function is not isolated from the rest of your program any more, and you have to check who has access to that value. That's a lot to keep track of. Second: Your function mutates a value. Now you have to keep track of everyone who references that value, and everywhere your function is invoked. In both situations, the number of scenarios you must test is greatly expanded compared to when you have a 'pure' function that does not operate on mutable memory. Referential transparency means that for a fixed input value you can replace a function invocation with a static value. It's just a mapping that is always the same, whether it's computationally expensive or not. That means that you can always expect the same behavior when you compose that function. But even more important, you can assert that your function is equal to something else -- always, under all conditions. This means that you can make a series of equational substitutions. And THAT means that you can use equational reasoning to prove things about your function. And if your program is just a bunch of functions that are composed together, well then you can prove things about your program, too. Programs are getting really complex. Really, really, really complex. Having the power to make more safe assertions about your programs is becoming more important. Being able to prove things about your programs using well known proving techniques, such as those borrowed from more formal maths like abstract algebra, is really useful. You still need to test, but what you need to test becomes of much narrower scope and much less cumbersome. This is why functional programming is indeed becoming more popular.
  - mden 11y ago
    If a function receives immutable state, returns immutable state, and does not depend or modify outside mutable state, then that function has no side effects. Mutating state within the function itself will not affect anything outside it and so mutations are not side effects, at least by default. About your two situations, I am guessing you mean that the functions rely on state not being passed in, but rather on state referenced from the outer scope? I agree that that complicates both reasoning and testing, and so it should be avoided. In C/C++ this type of design (i.e. relying on static scope state) is practically always avoided as there's rarely any need for it. If instead you mean that mutable references are being passed in as parameters then logic wise isn't this similar to assignment/binding in a functional language as long as you avoid propagating the side effect to other functions? I am personally a great fan of immutability, just not functional languages. I can see the justification for limiting the tools at your disposable to guarantee certain things, it's just that in this case I think they are not sufficient. --- For those downvoting, gee thanks. I see how trying to have a discussion is hurting your feelings.
    - sink 11y ago
      Yeah! If your mutability is completely limited to the scope of your function, then you should be fine. If your programming language takes the power to mutate away from you then you have even less to worry about: You don't have to rely on self-discipline to not write a bad program, the compiler tells you it's not good. Even in really small functions, with tiny scopes, I think reasoning about mutation takes a tidy mental toll. You can express about almost everything you need (well, I don't really know you or what you are programming) with maps and folds and recursion. In object oriented languages the traditional belief has been that encapsulation with privacy modifiers and getters and setters is sufficient to make well behaved programs. I don't think that goes far enough. I think that to reason about programs effectively you need some sort of immutability guarantee.
  - mpweiher 11y ago
    That's just handwaving. Assume for a second that your reader knows about referential integrity, has taken advanced FP in university, programmed in/with and implemented higher order mechanisms. Assume that the reader also knows how substitutability makes some variants of FRP much, much harder to both implement and reason about, has Haskell code in production that only two people at the company claim to understand, knows about the Principle of Least Expressiveness": "When programming a component, the right computation model for the component is the least expressive model that results in a natural program." And also knows about how to interpret it, namely: "Note that it doesn't say to always use the least possible expressive model; that will result in unnatural (awkward, hard to write, hard to read) programs in at least some cases" (http://c2.com/cgi/wiki?PrincipleOfLeastPower http://c2.com/cgi/wiki?PrincipleOfLeastPower) Assume that the person has seen people be very productive with simple dataflow tools such as Quartz Composer, and then hit a wall because that simpler programming model doesn't just have a low threshold, it also has a low ceiling. And has read in a report on 15+ years of constraint programming that students consistently found it difficult to think ("reason") in a functional style. (see http://blog.metaobject.com/2014/03/the-siren-call-of-kvo-and-cocoa-bindings.html http://blog.metaobject.com/2014/03/the-siren-call-of-kvo-and...) So. What evidence do you have for your assertions? Not arguments or logical inferences from your assumptions, but actual evidence?
zak_mc_kracken 11y ago
A program that's harder to prove correct is not necessarily incorrect. I'd actually argue that most of the software that runs our lives today is impossible to prove correct and yet seems to be doing quite alright overall. You're setting up a similar false dichotomy as people who say that programs that ship without automated tests are worthless and broken.
- sink 11y ago
  Nah, I am saying two things: 1. Mutability makes your program harder to reason about. 2. There are better ways to spend your time than writing tests for conditions that could not exist with pure functions. You could totally extrapolate a ton of statements from those two statements though. But I'm not doing that now, and not here.
  - mpweiher 11y ago
    > 1. Mutability makes your program harder to reason about. How so?
    - sink 11y ago
      I give an example in a sibling (cousin?) comment here: https://news.ycombinator.com/item?id=9372280 https://news.ycombinator.com/item?id=9372280
mpweiher 11y ago
You are conflating "proving correct", which is exceedingly rare and "reason about", which is extremely common.` Functional languages may make the former easier (though from the proofs we did in University, I don't really see it), but they make the latter much harder in many cases.
- sink 11y ago
  I disagree. I think reasoning in a programming language that limits effects with types and promotes partitioning them from the rest of your logic is dramatically simpler than in languages where mutation and effects can happen anywhere.
  - mpweiher 11y ago
    > mutation and effects can happen anywhere. That's a red herring and a scare-story that FPers tell each other. They can't happen "anywhere". They happen where you tell them to happen. Do you have any evidence that actual reasoning is simpler? "At the end you usually get a tight loop that is easy to follow. It is also much more imperative/operational than before, which may bug Haskell-style people." -- Jonathan Blow https://twitter.com/jonathan_blow/status/588007366618062848 https://twitter.com/jonathan_blow/status/588007366618062848 "I wanted to see how hard it was to implement this sort of thing in Go, with as nice an API as I could manage. It wasn't hard. Having written it a couple of years ago, I haven't had occasion to use it once. Instead, I just use "for" loops. You shouldn't use it either." -- Rob Pike https://github.com/robpike/filter https://github.com/robpike/filter This matches my experience pretty well. When I first created Higher Order Messaging, I was also really into creating chained higher order ops. After a little while, I noticed that a small for-loop was actually more readable than the really cool filter-chains I had created. Less cool, but more readable, comprehensible, easier to reason about, not least because of named intermediate values, something that tends to get lost in point-free style (and trust me, having been a heavy user + implementor of Postscript, I know a little about point-free style).
    - sink 11y ago
      In a strongly typed functional program I can prove that side effects only happen in specific places that are designated by the types. I have no such assistance in say Java, or Python. That is what I mean that side effects can happen anywhere. I would call referential transparency, which gives rise to equational reasoning, very strong evidence that reasoning becomes simpler.

by sink 11y ago

mden 11y ago

"[They] break referential equality and equational reasoning" Please explain? Mutations can cause side-effects but don't have to. You seem to think that limiting program behavior _necessarily_ alleviates informal reasoning, but that's not the case. Your argument is also highly hyperbolic in terms of testing. A properly designed system with immutability needs to be tested no less than properly designed system with mutability.

sink 11y ago
Sure! Mutations ARE side effects. Consider two situations with a function and a mutable variable: First: Your function depends on a value that can mutate. Now you have a hidden parameter to your function. You have to test the function under all reasonable conditions by which the value can change. The function is not isolated from the rest of your program any more, and you have to check who has access to that value. That's a lot to keep track of. Second: Your function mutates a value. Now you have to keep track of everyone who references that value, and everywhere your function is invoked. In both situations, the number of scenarios you must test is greatly expanded compared to when you have a 'pure' function that does not operate on mutable memory. Referential transparency means that for a fixed input value you can replace a function invocation with a static value. It's just a mapping that is always the same, whether it's computationally expensive or not. That means that you can always expect the same behavior when you compose that function. But even more important, you can assert that your function is equal to something else -- always, under all conditions. This means that you can make a series of equational substitutions. And THAT means that you can use equational reasoning to prove things about your function. And if your program is just a bunch of functions that are composed together, well then you can prove things about your program, too. Programs are getting really complex. Really, really, really complex. Having the power to make more safe assertions about your programs is becoming more important. Being able to prove things about your programs using well known proving techniques, such as those borrowed from more formal maths like abstract algebra, is really useful. You still need to test, but what you need to test becomes of much narrower scope and much less cumbersome. This is why functional programming is indeed becoming more popular.
- mden 11y ago
  If a function receives immutable state, returns immutable state, and does not depend or modify outside mutable state, then that function has no side effects. Mutating state within the function itself will not affect anything outside it and so mutations are not side effects, at least by default. About your two situations, I am guessing you mean that the functions rely on state not being passed in, but rather on state referenced from the outer scope? I agree that that complicates both reasoning and testing, and so it should be avoided. In C/C++ this type of design (i.e. relying on static scope state) is practically always avoided as there's rarely any need for it. If instead you mean that mutable references are being passed in as parameters then logic wise isn't this similar to assignment/binding in a functional language as long as you avoid propagating the side effect to other functions? I am personally a great fan of immutability, just not functional languages. I can see the justification for limiting the tools at your disposable to guarantee certain things, it's just that in this case I think they are not sufficient. --- For those downvoting, gee thanks. I see how trying to have a discussion is hurting your feelings.
  - sink 11y ago
    Yeah! If your mutability is completely limited to the scope of your function, then you should be fine. If your programming language takes the power to mutate away from you then you have even less to worry about: You don't have to rely on self-discipline to not write a bad program, the compiler tells you it's not good. Even in really small functions, with tiny scopes, I think reasoning about mutation takes a tidy mental toll. You can express about almost everything you need (well, I don't really know you or what you are programming) with maps and folds and recursion. In object oriented languages the traditional belief has been that encapsulation with privacy modifiers and getters and setters is sufficient to make well behaved programs. I don't think that goes far enough. I think that to reason about programs effectively you need some sort of immutability guarantee.
- mpweiher 11y ago
  That's just handwaving. Assume for a second that your reader knows about referential integrity, has taken advanced FP in university, programmed in/with and implemented higher order mechanisms. Assume that the reader also knows how substitutability makes some variants of FRP much, much harder to both implement and reason about, has Haskell code in production that only two people at the company claim to understand, knows about the Principle of Least Expressiveness": "When programming a component, the right computation model for the component is the least expressive model that results in a natural program." And also knows about how to interpret it, namely: "Note that it doesn't say to always use the least possible expressive model; that will result in unnatural (awkward, hard to write, hard to read) programs in at least some cases" (http://c2.com/cgi/wiki?PrincipleOfLeastPower http://c2.com/cgi/wiki?PrincipleOfLeastPower) Assume that the person has seen people be very productive with simple dataflow tools such as Quartz Composer, and then hit a wall because that simpler programming model doesn't just have a low threshold, it also has a low ceiling. And has read in a report on 15+ years of constraint programming that students consistently found it difficult to think ("reason") in a functional style. (see http://blog.metaobject.com/2014/03/the-siren-call-of-kvo-and-cocoa-bindings.html http://blog.metaobject.com/2014/03/the-siren-call-of-kvo-and...) So. What evidence do you have for your assertions? Not arguments or logical inferences from your assumptions, but actual evidence?

zak_mc_kracken 11y ago

A program that's harder to prove correct is not necessarily incorrect. I'd actually argue that most of the software that runs our lives today is impossible to prove correct and yet seems to be doing quite alright overall. You're setting up a similar false dichotomy as people who say that programs that ship without automated tests are worthless and broken.

sink 11y ago
Nah, I am saying two things: 1. Mutability makes your program harder to reason about. 2. There are better ways to spend your time than writing tests for conditions that could not exist with pure functions. You could totally extrapolate a ton of statements from those two statements though. But I'm not doing that now, and not here.
- mpweiher 11y ago
  > 1. Mutability makes your program harder to reason about. How so?
  - sink 11y ago
    I give an example in a sibling (cousin?) comment here: https://news.ycombinator.com/item?id=9372280 https://news.ycombinator.com/item?id=9372280

mpweiher 11y ago

You are conflating "proving correct", which is exceedingly rare and "reason about", which is extremely common.` Functional languages may make the former easier (though from the proofs we did in University, I don't really see it), but they make the latter much harder in many cases.

sink 11y ago
I disagree. I think reasoning in a programming language that limits effects with types and promotes partitioning them from the rest of your logic is dramatically simpler than in languages where mutation and effects can happen anywhere.
- mpweiher 11y ago
  > mutation and effects can happen anywhere. That's a red herring and a scare-story that FPers tell each other. They can't happen "anywhere". They happen where you tell them to happen. Do you have any evidence that actual reasoning is simpler? "At the end you usually get a tight loop that is easy to follow. It is also much more imperative/operational than before, which may bug Haskell-style people." -- Jonathan Blow https://twitter.com/jonathan_blow/status/588007366618062848 https://twitter.com/jonathan_blow/status/588007366618062848 "I wanted to see how hard it was to implement this sort of thing in Go, with as nice an API as I could manage. It wasn't hard. Having written it a couple of years ago, I haven't had occasion to use it once. Instead, I just use "for" loops. You shouldn't use it either." -- Rob Pike https://github.com/robpike/filter https://github.com/robpike/filter This matches my experience pretty well. When I first created Higher Order Messaging, I was also really into creating chained higher order ops. After a little while, I noticed that a small for-loop was actually more readable than the really cool filter-chains I had created. Less cool, but more readable, comprehensible, easier to reason about, not least because of named intermediate values, something that tends to get lost in point-free style (and trust me, having been a heavy user + implementor of Postscript, I know a little about point-free style).
  - sink 11y ago
    In a strongly typed functional program I can prove that side effects only happen in specific places that are designated by the types. I have no such assistance in say Java, or Python. That is what I mean that side effects can happen anywhere. I would call referential transparency, which gives rise to equational reasoning, very strong evidence that reasoning becomes simpler.