Wadler's Blog

Cute Phil - love the end
 

With all respect to Wadler, Edinburgh University, Java and ML, I am still terrified when I see mentioning of Russia as synonym of abstract "enemy". Dear Prof. Wadler! Your audience is international! Stop being rude!
 

I didn't mention Russia as an "abstract enemy", I mentioned it because every fraud incidents of this kind that I've heard involved surreptitiously wiring funds to Russia. Admittedly, it's out of date, as the incidents I remember are a few years old and involved pc's rather than phones. If folk know of more recent incidents, involving whatever locality, please post here.
 

Remind me - how do strongly typed variables stop the Russian Business Network from stealing my credit card number?
 

In Soviet Russia balanced ternary compares you!
 

I am sorry to say that your example is misleading. Type checking happens at compile and can thus NOT protect you machine at runtime. There is no guarantee whatsover that what you download has been compiled with that compiler! The only means to ensure the kind of security you refer to are dynamic checks at runtime.
I am sure you can do amazing stuff with formal logics, but protecting running systems will always require runtime checks.
 

In response to akuhn: You are correct that runtime checks are also needed, but static type checking is a crucial component of the Java security model. For instance, it is not possible to impose a dynamic arrays bound check (essential to avoiding buffer overflow exploits) unless you know which values are of type array.

Indeed, I don't know any secure system that does not use types; although some of them, such as Scheme, use a type system that is dynamically rather than statically enforced. Scheme is of particular interest because of the Scheme community's experiments with intermixing static and dynamic type checking.