3 ms·

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

by 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.

mpweiher 11y ago
You're still conflating "prove" with "reason". I don't need to prove things about my code in order to reason about it. For example, I can just look at the code in question to know whether it has side effects, and most code doesn't. In fact, most proofs I have seen don't particularly help me reason about the code in question. On the other hand, a simple imperative execution model does help me reason about the code.
- sink 11y ago
  I don't think I am doing any such conflating. Being able to reason about things equationally makes my code easier to reason about. Having a type system and a compiler assist me makes my code easier to reason about. Having fewer variants makes my code easier to reason about. Not needing to know the order in which functions have been invoked to know their return values makes my code easier to reason about. However, I will make the statement -- and this is indeed conflating! -- If I can prove something about my code, then it is easier to reason about. The proof can be simple or complex.
  - mpweiher 11y ago
    Again, you are just repeating your assertions and somehow think that simply asserting them makes them true. It does not, and I don't think I can make you understand the difference between assertions and evidence, so let's call it a day.
    - deleted 11y ago
      [deleted]
    - sink 11y ago
      I think my assertions are pretty well accepted virtually ... everywhere, so it didn't really occur to me THOSE specifically were what you were calling into question. But if THAT is what we are arguing about, I agree, this is all rather cyclical and pointless.
      - mpweiher 11y ago
        They're not. Or rather, you have a very narrow definition of "everywhere". And even if they were, that doesn't make them true without evidence, quite the contrary, that makes them especially suspect (groupthink etc.). Also, if you're so sure they are universally accepted, why the need to argue them at all? And of course, if they are so universally true, it should be trivial to actually come up with actual evidence, which hasn't been the case. Something to think about. Maybe.

by sink 11y ago

mpweiher 11y ago

You're still conflating "prove" with "reason". I don't need to prove things about my code in order to reason about it. For example, I can just look at the code in question to know whether it has side effects, and most code doesn't. In fact, most proofs I have seen don't particularly help me reason about the code in question. On the other hand, a simple imperative execution model does help me reason about the code.

sink 11y ago
I don't think I am doing any such conflating. Being able to reason about things equationally makes my code easier to reason about. Having a type system and a compiler assist me makes my code easier to reason about. Having fewer variants makes my code easier to reason about. Not needing to know the order in which functions have been invoked to know their return values makes my code easier to reason about. However, I will make the statement -- and this is indeed conflating! -- If I can prove something about my code, then it is easier to reason about. The proof can be simple or complex.
- mpweiher 11y ago
  Again, you are just repeating your assertions and somehow think that simply asserting them makes them true. It does not, and I don't think I can make you understand the difference between assertions and evidence, so let's call it a day.
  - deleted 11y ago
    [deleted]
  - sink 11y ago
    I think my assertions are pretty well accepted virtually ... everywhere, so it didn't really occur to me THOSE specifically were what you were calling into question. But if THAT is what we are arguing about, I agree, this is all rather cyclical and pointless.
    - mpweiher 11y ago
      They're not. Or rather, you have a very narrow definition of "everywhere". And even if they were, that doesn't make them true without evidence, quite the contrary, that makes them especially suspect (groupthink etc.). Also, if you're so sure they are universally accepted, why the need to argue them at all? And of course, if they are so universally true, it should be trivial to actually come up with actual evidence, which hasn't been the case. Something to think about. Maybe.