Image

Luca Cardelli was born near Montecatini Terme, Italy, studied at the University of Pisa and has a Ph.D. in computer science from the University of Edinburgh . He worked at Bell Labs, Murray Hill, from 1982-04-05 to 1985-09-20, and at Digital Equipment Corporation, Systems Research Center in Palo Alto, from 1985-09-30 to 1997-10-31.he is currently Principal Researcher and head of the Programming Principles and Tools and Security groups.

 His main interests are in type theory and operational semantics , and in concurrency theory . He implemented the first compiler for ML ,one of the most popular typed functional language. He was a member of the Modula-3 design committee, and has designed a few experimental languages, including Obliq.

 

He has published over 100 papers, 1 book, and 3 conference proceedings as chair/editor . He has served in over 80 Program Committees, and as editor of Theoretical Computer Science ,

 

 

 

 

Type Systems

 

Luca Cardelli

Microsoft Research

 

 Introduction

The fundamental purpose of a type system is to prevent the occurrence of execution errors duringthe running of a program. This statement motivates the study of type systems. Its accuracy depends, first of all, on the rather subtle issue of what constitutesan execution error, which we will discuss in detail. Even when that is settled, the absence

of execution errors is a nontrivial property. When such a property holds for all of the program runs that can be expressed within a programming language, we say that the language is type sound. It turns out that a fair amount of careful analysis is required to avoid false and embarrassing claims of type soundness for programming languages. As a consequence, the classification,description, and study of type systems has emerged as a formaldiscipline.

The formalization of type systems requires the development of precise

notations and definitionsand the detailed proof of formal properties that give confidence in the appropriateness

of the definitions. Sometimes the discipline becomes rather abstract. One should always remember,though, that the basic motivation is pragmatic: the abstractions have arisen out of necessity and can usually be related directly to concrete intuitions. Moreover, formal techniques need not be applied in full in order to be useful and influential. A knowledge of the main principles of type systems can help in avoiding obvious and not so obvious pitfalls, and can inspire regularity

and orthogonality in language design.

When properly developed, type systems provide conceptual tools with which to judge the adequacy of important aspects of language definitions. Informal language descriptions often fail to specify the type structure of a language in sufficient detail to allow unambiguous implementation.

It often happens that different compilers for the same language implement slightly different type systems. Moreover, many language definitions have been found to be type unsound, allowing a program to crash even though it is judged acceptable by a typechecker. Ideally, formaltype systems should be part of the definition of all typed programming languages. This way,typechecking algorithms could be measured unambiguously against precise specifications and,if at all possible and feasible, whole languages could be shown to be type sound.In this introductory section we present an informal nomenclature for typing, execution errors, and related concepts. We discuss the expected properties and benefits of type systems, and we review how type systems can be formalized. The terminology used in the introduction is not completely standard; this is due to the inherent inconsistency of standard terminology arising from various sources. In general, we avoid the words type and typing when referring to run time

concepts; for example we replace dynamic typing with dynamic checking and avoid common but ambiguous terms such as strong typing. The terminology is summarized in the Defining

 Execution errors and safety

It is useful to distinguish between two kinds of execution errors: the ones that cause the computation

to stop immediately, and the ones that go unnoticed (for a while) and later cause arbitrary

behavior. The former are called trapped errors, whereas the latter are untrapped errors.

An example of an untrapped error is improperly accessing a legal address, for example, accessing data past the end of an array in absence of run time bounds checks.

  Another untrappederror that may go unnoticed for an arbitrary length of time is           jumping to the wrong address:

      memory there may or may not represent an instruction stream. Examples of trapped errors are

 division by zero and accessing an illegal address:

      the computation stops immediately (on many

computer architectures).

 A program fragment is safe if it does not cause untrapped errors to occur. Languages where all program fragments are safe are called safe languages. Therefore, safe languages rule out the most insidious form of execution errors: the ones that may go unnoticed. Untyped languages may enforce safety by performing run time checks. Typed languages may enforce safety by statically rejecting all programs that are potentially unsafe. Typed languages may also use a mixture of run time and static checks.Although safety is a crucial property of programs, it is rare for a typed language to be concerned exclusively with the elimination of untrapped errors. Typed languages usually aim to rule out also large classes of trapped errors, along with the untrapped ones.

Execution errors and well-behaved programs

For any given language, we may designate a subset of the possible execution errors as forbidden errors. The forbidden errors should include all of the untrapped errors, plus a subset of the trapped errors. A program fragment is said to have good behavior, or equivalently to be well behaved, if it does not cause any forbidden error to occur. (The contrary is to have bad behavior, or equivalently to be ill behaved.) In particular, a well behaved fragment is safe.A language where all of the (legal) programs have good behavior is called strongly checked.Thus, with respect to a given type system, the following holds for a strongly checked language:

• No untrapped errors occur (safety guarantee).

• None of the trapped errors designated as forbidden errors occur.

• Other trapped errors may occur; it is the programmer’s responsibility to avoid them.

Typed languages can enforce good behavior (including safety) by performing static (i.e.,

compile time) checks to prevent unsafe and ill behaved programs from ever running. These languages

are statically checked; the checking process is called typechecking, and the algorithm

that performs this checking is called the typechecker. A program that passes the typechecker is

said to be well typed; otherwise, it is ill typed, which may mean that it is actually ill-behaved,

The issue of whether programming languages should have types is still subject to some debate.

There is little doubt that production code written in untyped languages can be maintained only

with great difficulty. From the point of view of maintainability, even weakly checked unsafe

languages are superior to safe but untyped languages (e.g., C vs. LISP). Here are the arguments

that have been put forward in favor of typed languages, from an engineering point of view:

Economy of execution : Type information was first introduced in programming to improve code generation and run time efficiency for numerical computations, for example, in FORTRAN. In ML, accurate type information eliminates the need for nil-checking on pointer dereferencing. In general, accurate type information at compile time leads to the application of the appropriate operations at run time without the need of expensive tests.

Economy of small-scale development:When a type system is well designed, typechecking

can capture a large fraction of routine programming errors, eliminating lengthy debugging

sessions. The errors that do occur are easier to debug, simply because large

classes of other errors have been ruled out. Moreover, experienced programmers adopt

a coding style that causes some logical errors to show up as typechecking errors: they

use the typechecker as a development tool. (For example, by changing the name of a

field when its invariants change even though its type remains the same, so as to get error

reports on all its old uses.)

Economy of compilation:Type information can be organized into interfaces for program

modules, for example as in Modula-2 and Ada. Modules can then be compiled independently

of each other, with each module depending only on the interfaces of the others.

Compilation of large systems is made more efficient because, at least when interfaces

are stable, changes to a module do not cause other modules to be recompiled.

 

Economy of large-scale development:Interfaces and modules have methodological advantages

for code development. Large teams of programmers can negotiate the interfaces

to be implemented, and then proceed separately to implement the corresponding

pieces of code. Dependencies between pieces of code are minimized, and code can be

locally rearranged without fear of global effects. (These benefits can be achieved also by

informal interface specifications, but in practice typechecking helps enormously in verifying

adherence to the specifications.)

 

Economy of development and maintenance in security areas.:

Although safety is necessary

to eliminate

other catastrophic security breaches. Here is a typical one: if there is any way at all,

no matter how convoluted, to cast an integer into a value of pointer type (or object type),

then the whole system is compromised. If that is possible, then an attacker can access

any data anywhere in the system, even within the confines of an otherwise typed language,

according to any type the attached chooses to view the data with. Another helpful

(but not necessary) technique is to convert a given typed pointer into an integer, and then

into a pointer of different type as above. The most cost effective way to eliminate these

security problems, in terms of maintenance and probably also of overall execution efficiency,

is to employ typed languages. Still, security is a problem at all levels of a system:

typed languages are an excellent foundation, but not a complete solution.

 

Economy of language features.:Type constructions are naturally composed in orthogonal

ways. For example, in Pascal an array of arrays models two-dimensional arrays; in

ML, a procedure with a single argument that is a tuple of n parameters models a procedure

of n arguments. Thus, type systems promote orthogonality of language feature

question the utility of artificial restrictions, and thus tend to reduce the complexity of

programming languages.

CLEARDESK PROJECT

Image

The ClearDesk Project(or), 1990-1997

Luca Cardelli and Ken Beckman, Digital Equipment Corporation, Systems Research Center

The ClearDesk projector currently rests in our Sub-Forum, where it can still be marveled at. Right above it, in the Forum, a modern large-screen projector dominates the room. Pull up a chair in front of it and pretend, just for a second, to be sitting behind your desk.

1. Science

The ClearDesk project was formulated during a time when many people at SRC acquired three displays on their desks, therefore making their desks completely useless for any other purposes. Well, we said, why not place one or more displays behind the desk, so as to clear up the desk surface? Hence the name of the project.

A display suitable for this use had to be big enough to be readable from behind one’s desk. To preserve the customary solid view angle, such a display had to be about 40″ diagonal. The only conceivable technology at the time was either front or back projection onto a large piece of glass. Front projection would have required attaching a massive harness to the ceiling, right over my head. After the Loma Prieta earthquake, this was somewhat unappealing. Therefore, we chose back projection. Never mind that this design would consume vast amounts of floor space; the follow-up project, ClearFloor, would fix all that.

A suitable display also had to be bright enough to be viewable under ordinary office lighting conditions, including coping with the summer light shining through our floor-to-ceiling windows. Mighty photons are required under those conditions, much mightier than one can get out of an overhead slide projector or a back-projection TV. Therefore, we chose a bright auditorium projector. It was a small step, from the personal computer to the personal auditorium.

2. Engineering

Our chosen projector (ElectroHome ECP 3000) was no doubt cutting-edge technology. Even without any knowledge of electronics, this fact could be inferred from the frequency with which the electronics failed. Moreover, the manual contained an interesting little footnote: if the light output was cranked up ever so slightly beyond specs, the projector could start emitting soft X-rays! Fortunately, our design provided for a vertically mounted projector with a 45-degree mirror to deflect the light towards the viewer. Soft X-rays go straight through optical mirrors (yes, we asked) and away from the viewer. In any case, we did it for Science.

The next pieces of technology we required were the materials along the optical path. It turns out that a 99% reflectance mirror is just ordinary stuff you can buy in almost any size. More problematic was the choice of the viewing surface. We tested several fancy Fresnel-like sheets of plastic, designed to concentrate light in nice parallel wavefronts instead of scattering it in all directions. Usually, this technique sends most light towards the viewers, making the picture brighter. However, at our unusual viewing distance these materials created a bright hot-spot in the middle of the picture, with most of the light zipping by our ears. We also tested a little piece of F-16 anti-glare cockpit glass (honest!), but this was just too dark and probably beyond our budget. We ended up using the cheapest piece of plain frosted glass we could find. This worked great, giving us equally good viewing from any angle.

So, now we had a state-of-the-art projector, an optical-quality mirror, a piece of cheap frosted glass, and a light path. All we needed was something to hold them in place. Enter the amazing UNISTRUT. This miracle of modern mechanical engineering beats Lego and Fisher-Price hands down. This is an industrial-strength erector set. My early experience with the kiddie version finally paid off. After much cutting and fastening (but no welding!), and much assistance from Chuck Needham, we had a sturdy frame to screw all the rest onto.

Eventually, one ClearDesk projector was assembled. It was designed so that if multiple units were built, they could be adjoined horizontally without any viewing gaps. Three units next to each other would have been fantastic. But I had had enough of mechanical engineering. Moreover, it turned out that the assembled unit was precisely large enough to pass through the door of my office, and I decided not to push my luck any further.

3. Social Impact

A ClearDesk-style display is obviously great for personal enjoyment, for giving demos to large groups of people, and for impressing random visitors. Just as obvious are the facts that focusing at a distance is easier on the eyes, and that a large display is easier to read for people with not-so-good eyesight. However, the ClearDesk projector had other unexpected uses.

First of all, if a job candidate did not comment on the display within 5 minutes of entering my office, that was a clear indication of a non-forward-thinking person. We have little use for such people here.

Second, the ClearDesk display was incredibly useful for cooperative work. A coauthor could sit by my side and comfortably view the paper I was editing, so we could work interactively instead of working on paper or squinting at a regular monitor. In fact, this is the way Martin Abadi and I spent much of our time while writing our book. Martin would use a laser pointer to indicate on the big screen were I should make corrections. Unless, that is, the correction happened to be in lower left corner of the display, because then the laser beam would bounce off the glass into my eyes. Martin was well trained to never, ever point there.

Most of all, I am proud of the fact that, well ahead of the current Carpal Tunnel Syndrom pandemic, we built the ultimate ergonomic computing environment . It pleases me to think that if just one person (i.e., me) was saved from CTS and back pain, then my company probably saved millions of dollars in legal fees, therefore compensating for the cost of the project many times over.

4. Decline and Fall

As a research project ClearDesk was very successful, being functional and well over 5 years ahead of the times. After frequent failures in the early years, the projector proved surprisingly reliable. In fact, it was eventually discovered that the electronics failed only when not being used. That is, the projector would work flawlessly for several months during which it would never be turned off. Then a general power failure would cause it lose power. If promptly powered up, everything would be fine. But if the power failure happened over a weekend or while I was in vacation, then, after more than a day of inactivity the projector would be D.O.P. (dead-on-power-up). After that discovery, prompt re-power-ups ensured years of uninterrupted service.

What finally retired the ClearDesk projector was not failing electronics, but rather the relentless march of technology, as well as the relentless stupidity of Apple Computer. For most of its life the projector was connected to a Macintosh, but Apple made it necessary to eventually connect it to a PC. Modern PC’s, however, switch resolution at least three times during booting, and this is not a pretty thing to watch on the ElectroHome projector. Moreover, the higher resolutions in use nowadays result in fuzzier pixels on older-technology projectors. So, it eventually came time to rearrange my furniture.

The ClearDesk projector currently rests in our Sub-Forum, where it can still be marveled at. Right above it, in the Forum, a modern large-screen projector dominates the room. Pull up a chair in front of it and pretend, just for a second, to be sitting behind your desk.

 ImageImage 

DNA COMPUTING AND MOLECULAR PROGRAMMING

Image 

 BOOKS

 

  A Theory of Objects
by Martin Abadi, Luca Cardelli

 

 

 DNA Computing and Molecular Programming:

 

Ecoop 2003 – Object-Oriented Programming:

 

Advertisements