What is a type error?

[Joachim Durchholz]

Marshall schrieb:
> Now, I'm not fully up to speed on DBC. The contract specifications,
> these are specified statically, but checked dynamically, is that
> right?

That's how it's done in Eiffel, yes.

 > In other words, we can consider contracts in light of
> inheritance, but the actual verification and checking happens
> at runtime, yes?

Sure. Though, while DbC gives rules for inheritance (actually subtypes), 
these are irrelevant to the current discussion; DbC-minus-subtyping can 
still be usefully applied.

> Wouldn't it be possible to do them at compile time? (Although
> this raises decidability issues.)

Exactly, and that's why you'd either uses a restricted assertion 
language (and essentially get something that's somewhere between a type 
system and traditional assertion); or you'd use some inference system 
and try to help it along (not a simple thing either - the components of 
such a system exist, but I'm not aware of any system that was designed 
for the average programmer).

 > Mightn't it also be possible to
> leave it up to the programmer whether a given contract
> was compile-time or runtime?

I'd agree with that, but I'm not sure how well that would hold up in 
practice.

Regards,
Jo