Herman Venter, programming language enthusiast

Is there a contract in your future?

In my previous posting I speculated that compile time type checkers as we know them today may fall by the wayside in favor of something that looks and feels a lot more like the dynamically typed languages.

One of the statements I made, “If you store an object in field foo and then call foo.bar(x, y, z), you really don’t care what the type of the object in foo is, only that it should have a function property called bar that can handle the arguments x, y and z.”, needs further qualification.

Yes, you do not care what the type of the object in foo is, nor do you care about the particular function value that is stored in the bar property. However, you do care about what exactly is going to happen when you call foo.bar(x, y, z). It is pretty hard to program if you do not know what your program is going to do.

In our current champion languages you get narrow things down by being specific about what types of values you may pass to bar and what type of value you can expect to get back. But that is a far cry from knowing what the function is going to do.

Much more useful is a precondition that states “before you call this function, the following things must be true” and a postcondition that states “if you call this function while satisfying the precondition, you can be sure that the following things will be true”.

Our current best practice is to state these conditions in documentation. Getting this documentation to be accurate and to stay accurate is quite a challenge. And much of the time we never quite get around to creating the documentation.

I am persuaded that a programming language that makes it really easy to write down these pre and post conditions (contracts) and that quickly and accurately checks that function implementations satisfy their contracts, will make programming easier and programmers more productive.

Just how this will be done is not obvious, but it is a worthy goal for anyone aspiring to come up with one or more of the innovations that will unlock the next champion programming language.
Published Wednesday, March 05, 2008 10:58 AM by hermanventer

Comments

 

ptorr said:

One thing that will be important for security is that contracts not just say "this will be true on exit" but also a guarantee that "...and nothing else will happen." Many security bugs are caused by unforseen side-effects of code, or subtle changes in behaviour made to code over time. Silly example: eval() guarantees that if you pass in a valid expression, it will return the correct result... but it fails to mention that it might also format your hard-drive if you pass in a different kind of source code. This is a highly contrived example, but it highlights how developers (fail to) think about security problems.

Unfortunately it is virtually impossible for the calling code to define a contract stating the totality of what can and cannot happen (or to even understand such a contract defined by the function implementor) since in theory the two pieces of code know nothing about each other and about what side-effects may or may not be acceptable. For example, the naive script developer would need to know that she needs to be worried about hard-drive formatting before she can correctly reason about the contracts / invariants needed for her program (which likely has nothing to do with hard drives at all).

Security systems such as the CLR deal with this specific example (don't let web apps have access to the hard drive) but they rely on a LOT of hard work under-the-covers to enforce the security semantics (web apps *do* access the hard drive, just not directly) and they don't protect against "algorithmic" security problems (those that can't be fixed by gating access to a specific resource).

From another angle, operating systems spend a large amount of time trying to abstract away the details of the underlying hardware, but those very details might be critical to the correct execution of the system (side-channel attacks on guessing AES keys, for example) even though in the vast majority of cases they will not be (hence the desire to have abstractions in the first place).

A more holistic approach to program behaviour, resoure utilisation, etc. is needed to create significantly more secure code, but that sounds like a daunting task!

May 15, 2008 4:12 PM
Anonymous comments are disabled

About hermanventer

Herman is a software developer in the Redmond laboratory of Microsoft Research. He joined Microsoft in 1998 as a software developer for Visual Studio, working on the JScript and JScript .NET compilers. Since then he has worked on compiler toolkits, Comega, Spec# and VerifiedC. View Herman Venter's profile on LinkedIn

© 2009 Microsoft Corporation. All rights reserved. Terms of Use  |  Trademarks  |  Privacy Statement
Microsoft
Page view tracker