What is a type error?

[David Hopwood]

Chris Smith wrote:
> David Hopwood <david.nospam.hopwood at blueyonder.co.uk> wrote:
> 
>>This is true, but note that postconditions also need to be efficient
>>if we are going to execute them.
> 
> If checked by execution, yes.  In which case, I am trying to get my head 
> around how it's any more true to say that functional languages are 
> compilable postconditions than to say the same of imperative languages.

A postcondition must, by definition [*], be a (pure) assertion about the
values that relevant variables will take after the execution of a subprogram.

If a subprogram is intended to have side effects, then its postcondition
can describe the results of the side effects, but must not reexecute them.


[*] E.g. see
    <http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf>,
    although the term "postcondition" was introduced later than this paper.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>