What is a type error?

[Marshall]

Joachim Durchholz wrote:
> Marshall schrieb:
> > Joachim Durchholz wrote:
> >> Chris Smith schrieb:
> >>> For example, I wrote that example using variables of type int.  If we
> >>> were to suppose that we were actually working with variables of type
> >>> Person, then things get a little more complicated.  We would need a few
> >>> (infinite classes of) derived subtypes of Person that further constrain
> >>> the possible values for state.  For example, we'd need types like:
> >>>
> >>>     Person{age:{18..29}}
> >>>
> >>> But this starts to look bad, because we used to have this nice
> >>> property called encapsulation.  To work around that, we'd need to
> >>> make one of a few choices: [...] (c) invent some kind of generic
> >>> constraint language so that constraints like this could be expressed
> >>> without exposing field names. [...] Choice (c), though, looks a
> >>> little daunting.
> >> That's not too difficult.
> >> Start with boolean expressions.
> >> If you need to check everything statically, add enough constraints that
> >> they become decidable.
> >
> > I'm not sure I understand. Could you elaborate?
>
> Preconditions/postconditions can express anything you want, and they are
> an absolutely natural extensions of what's commonly called a type
> (actually the more powerful type systems have quite a broad overlap with
> assertions).
> I'd essentially want to have an assertion language, with primitives for
> type expressions.

Now, I'm not fully up to speed on DBC. The contract specifications,
these are specified statically, but checked dynamically, is that
right? In other words, we can consider contracts in light of
inheritance, but the actual verification and checking happens
at runtime, yes?

Wouldn't it be possible to do them at compile time? (Although
this raises decidability issues.) Mightn't it also be possible to
leave it up to the programmer whether a given contract
was compile-time or runtime?

I've been wondering about this for a while.


Marshall