> If you are aiming for static type correctness (i.e. no "message not > understood" errors at runtime), you clearly need a type language you > can effectively reason about. One example of expressive but complex > type systems is the Flint project at Yale[1]. That system is undecidable, right? Viktor