Incremental addition of types and contracts

MSDN Channel9 has an excellent interview between Erik Meijer and Shriram Krishnamurthi which includes, among other things, a discussion of adding types, contracts, and verification to at least some portion of existing programs written in non-typed languages. I was especially interested by his claim that this was necessarily a problem of refactoring.

I often work in untyped languages and have learned to refactor by separating side-effects from logic, but I am curious about ways of adding contracts and type checking to portions of programs after they are written. Does anyone know of systems or papers addressing this topic?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

cool!

i haven't watched it yet, but those are some cool speakers, thanks for pointing it out. (there's a lot on c9 that sounds great, i just wish they would bloody well get some automatic speach-to-text transcripts going. i hate sitting through video/audio, i just want to read things.)

Typed Scheme

You might have a look at Typed Scheme and the related paper, The Design and Implementation of Typed Scheme, by Sam Tobin-Hochstadt and Matthias Felleisen from POPL 2008.

The idea is precisely to allow you to gracefully add (explicit) typing to a Scheme program, one module at a time.

Erlang is rich

i think Erlang is a great place to see pragmatic optional/gradual typing. i don't know of another language that comes close (but i don't know much so i might just be ignorant):

Dialyzer.

TypEr.

Quick Check (ok not really about types per se but still cool :-).