[TYPES] [tag] Re: Declarative vs imperative

[Uday S Reddy]

Mark Janssen writes:

> But if we're going to be in the Computer Science department, can we
> get away from the idea of "logic as a regimentation of natural
> language" (which is fine for the Philosophy department) and move to
> the idea of logic as equations of Binary Artihmetic and Boolean
> Algebra?

Oh, no!  Wherever you have learnt logic from, I am afraid they didn't do a
very good of explaining what logic is about (which is not unusual).

As Marc Denecker alluded to, logic is essentially a study of the information
content of statements.  The "information content" idea is formalized in
terms of consequence: which statement is a consequence of which other
statements.  If B is a consequence of A, i.e., if B necessarily happens to be
true in all situations where A is true, we understand that the information
contained in B is already contained in A.

Programming languages are also regimentations of natural language, albeit a
different part of natural language than the one classical logic has
traditionally concerned itself with.  When I was taught programming in the
70's, I was encouraged to use natural language for writing algorithms
because it helps you to think better.  (However, using natural language
correctly, i.e., precisely and unambiguously, requires quite a bit of
mathematical training, which is becoming increasingly rare in recent times.)

Programming logic is the logic used for reasoning about programs.  There, we
are interested not only in the consequences of statements, but also the
consequences of commands (or functions, operations or whatever).

We use natural language to communicate (and to think in) every day.  It is
obviously not meant for just the philosophers!

Cheers,
Uday