5 ms·
Yes, well said. Math is not any form of programming, and programming is not math. Studying the relations between the two can be very helpful, and the difference
by hyperjeff 7y ago
Yes, well said. Math is not any form of programming, and programming is not math. Studying the relations between the two can be very helpful, and the difference itself is interesting. One may have specific reasons to us FP to cleanly decouple from certain kinds of side-effects, but there’s nothing un-mathy about mutability, and there are times when it’s a fine choice.
- brianberns 7y agoCan you provide an example of mutability in, say, high school or undergraduate math?
- mlevental 7y agoany sum with an index of summation requires mutability
- chobytes 7y ago"requires" is a strong word. the only explicit definition ive seen given for n-ary summations and products products was recursive.
- brianberns 7y agoI don't think so. For example, sum of first 5 integers: sum i = 1 to 5 of i -> 1 + 2 + 3 + 4 + 5 = 15 Nothing mutable there. In functional programming this is done with a `fold`, which doesn't use mutation.
- pron 7y agoWe're talking about notation. Anything could be described in any Turing complete language. It's uncommon to have something similar to mutation in ordinary mathematical notation, but summation is one example where it's used.
- mruts 7y agoI mean, that’s exactly what the Curry-Howard Isomorphism says: that math and programming are equivalent. Both can express and are equivalent to Turing machines.
- pron 7y agoThat is not what the Curry-Howard Isomorphism -- AKA propositions-as-types -- says. Propositions-as-types is the observation that the typing rules of certain type systems follow the inference rules of certain logics (largely because they were designed this way), and that in general typing rules and inference rules can be made to mimic one another, so that a type system can represent propositions in some logic, and type checking represent proof-checking. That arbitrary mathematical proofs can be equivalently made by Turing machines (and conversely, that predicate calculus is Turing complete) is a lemma by Turing, published in the same 1936 paper in which he introduced the notion of computation, Turing machines and proved what today is known as the halting problem.