Lambda the Ultimate

When I learned Python in 1999 it was advertised, among other things, as "executable pseudo code". At my universities numerical studies we used a Pascal style pseudo code notation. Maybe it was even actually Pascal, I don't remember exactly. I didn't question a non-standard notation that changed from author to author which looked like imperative programming language syntax and was understood like imperative code but aimed to represent intentions better than any actual programming language.

Over the years I began to wonder about this pseudo-code idealism, how it became a common practice and why it is still used today? Any thoughts?

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?

This is a question that I encounter frequently when thinking about OOP and modules.

Say, I define a method m on some class inside a module M.

Should the method lookup table of the class contain an entry named "m" or "M::m"?

"M::m" seems cleaner, and more modular... whereas "m" seems more OO.