[TYPES] Declarative vs imperative

[Uday S Reddy]

Mark Janssen writes:

> The symbolic computing crowd seems to be completely different that all
> of that and is not addressed in the above.  There the "low-level" ends
> at the symbols themselves, not logic gates.

Indeed, you understand the point perfectly now.  One of Dijkstra's greatest
aphorisms was:

  It is not the job of our programs to instruct the computer.
  Rather, it is the job of the computer to execute our programs.

"Our programs" come the first and last.  The computer is there to dutifully
execute what we want done.

Whether the program achieves its goals or not is a black-and-white question,
which is settled even before the computer gets into the game.  

That is philosophically speaking.  In practice, we may have no practical way
to settle the question ahead of time.  We may need to test things out on the
computer to see whether our programs behave the way we want them to.
However, in principle, if we spent the time and effort to think through
every step and check every detail, we could have settled the question.  We
use the computer merely as a substitue for the lack of diligence on our
part.

Cheers,
Uday