Re: Redefinition of Equality (Long)

[Robb Nebbe <nebbe@iam.unibe.ch>]

Robert A Duff wrote:

> Well, the goal is to make sure that the compiler can *check* that the
> abstract value of an 'in' parameter is not modified. 
 
> ... And any time you
> want to check things at compile time, you have to put up with rules that
> are more pessimistic than they might be. 

In this particular case you may be right but I wouldn't expect this
to be true in general. I am sort of plucking this out of context but
I have seen other people say similar things. 

There is nothing intrinsic in compile time checking of semantic
properties that makes it necessarily pessimistic. In terms of model
theory (the branch of metamathematics that deal with these kinds of
issues) your statement is the equivalent of saying that no logic
(think logical system) can ever be both sound (~safe) and complete
(~not pessimistic) which is known to be false.

In a real language it might be the case that something isn't decidable
in which case you must choose to err on the side of safety or
expressiveness with dynamic checks to compensate. Or it might be
possible but just too complicated to be worth the effort. Or it just
might be that it isn't currently known how to do the checks.

Robb Nebbe