Typing for the programmer's convenience

[Reginald Braithwaite-Lee <address@hidden>]

Neel did a great job of explaining how ML-style type inference helps
the compiler. As I undestand it, his Needle language also tries to
provide a helpful explanation to the programmer when the compiler is
able to detect an inconsistency in types.

This latter facility interests me far more than using types to help the
compiler. In C++, there's a small performance benefit from using const:
the compiler can perform more optimizations when you provide hints.

However, the huge benefit of 'const correctness' lies in enforcing
constraints on the program's behaviour. You find more errors when you
write const-correct programs and think through your intentions more
thoroughly.

(This is analagous to Eiffel's "Design by Contract")

Is anyone working on typing systems from the perspective of program
correctness? Can anyone provide some reference materials for study?

Thanks in advance...

--
Reginald Braithwaite-Lee
<www.braithwaite-lee.com>

A recent newsgroup article said of a magazine, "Everything in [the
magazine] is an advertisement, and some of them are marked as such."


__________________________________________________
Do you Yahoo!?
Yahoo! Web Hosting - Let the expert host your site
http://webhosting.yahoo.com