What's this I hear about ML having all the nasty constructs of
other languages (like loops, else - if ladders). Is this because
many problems simply can't be implemented without the use of these
constructs or is it a facility for "quick dirty code" for programmers
who are not interested in proving their software?
So far as I know there is a while loop, I've never
used it.
We do not need loops, recursion will always do the job.
Consider the while loop
while B do S;Where B is a boolean expression and S is a statement. We model the action of S by changing some data state space DS. The program fragment above might be rewritten
while fB(DS) do DS := fS(DS);where fB and fS are proper functions which take in the data state DS and return appropriate values. DS might include all the global and local variables of the program. This program fragment may now be modelled with ML
fun while fB fS DS = if fB DS then (while fB fS (fS DS)) else DS;If then else ladders are there and it's OK to use them - pattern matching is preferred but it's not always convenient (I suspect not always possible). If _ then _ else _ introduces a new complexity to proofs - but it's not a serious problem.
If the former is true then surely the use of ML will continue to
be very scarce. If the latter is true then it seems that any language
(including C) which has these nasty contructs removed (or just
avoided by the lecturer!) can be proved as easily as ML.
Latter - yes, you could build ML by taking the bad
bits from C and adding a few new good bits. In the
end all languages are more or less the same.