Post by s***@gmail.comI has always been thinking this, but I need a confirmation: The
purpose of functional programming is to make written program becomes
a mathematical proof. Once a program is correctly written, it is
"proved" and is expected to work the same in any environment. This
is why in FP, immutable is needed, otherwise there's no guarantee
for the correctness of the "proof", because state changes can
introduce unexpected behaviors.
Am I correct on the basis of Functional Programming?
Yes and no. It's certainly possible to reason about changes of state,
and people like Dijkstra, Gries, Hoare have studied proof patterns for
such programs in the past. One wants to write even the imperative
program in such a way that the changes are not unexpected.
But immutability makes reasoning easier. Consider, absent knowledge
about f except assume that f does return:
{ String s = new String("whatever"); // immutable strings
f(s);
if (s.length() == 0) loop(); else halt(); }
{ String s = new String("whatever");
f(s);
if (s[0] == '?') loop(); else halt(); }
(let ((s (string-copy "whatever"))) ; mutable strings of constant length
(f s)
(if (zero? (string-length s)) (loop) (halt)))
(let ((s (string-copy "whatever")))
(f s)
(if (char=? (string-ref s 0) #\?) (loop) (halt)))
In neither language can f assign a different object to the local
variable s, so that helps some: we are reasoning about a known string
object that was the initial value of s.
In Java, f cannot change the String object at all, so that helps more:
both Java examples take the else branch.
In Scheme, f can change the first character to #\?, so it's not
possible to tell which branch the second Scheme example takes. The
first Scheme example takes the else branch, and a Scheme compiler
could in principle rely on that, assuming standard bindings.
In a functional language, just calling f for effect would make no
sense. There would be some local code to tell what the effect of f
might be, and that would then help in the reasoning. I think.