Understanding Computation (58 page)

This chapter has sketched the basic idea of
abstract interpretation—using cheap approximations to learn
about the behavior of expensive computations—and showed a simple type
system as an example of how approximations can be useful for analyzing
programs.

Our discussion of abstract interpretation was very informal.
Formally, abstract interpretation is a mathematical technique where
different semantics for the same language are connected together by
functions that convert collections of concrete values into abstract ones
and vice versa, allowing the results and properties of abstract programs
to be understood in terms of concrete ones.

A notable industrial application of this technique
is the
Astrée
static analyzer
, which uses abstract interpretation to
automatically prove that a C program is free of runtime errors like division by zero,
out-of-bounds array indexing, and integer overflow.
Astrée
has been used to verify the flight control software of Airbus A340 and
A380 airplanes, as well as the automatic docking software for the
Jules
Verne
ATV-001 mission that transported supplies to the International Space
Station. Abstract interpretation respects Rice’s theorem
by providing safe approximations rather than guaranteed answers, so
Astrée
has the potential to report a possible runtime error
where none actually exists (a
false alarm
); in practice, its
abstractions were precise enough to avoid any false alarms when verifying the A340
software.

Programs written in the
Simple
language can only
manipulate rudimentary values—numbers and Booleans—so the types seen in this chapter are very
basic. Real programming languages handle a wider variety of possible values, so real static
type systems are more sophisticated. For example, statically typed functional programming
languages like ML and Haskell have values that are functions (like Ruby’s procs), so their
type systems support
function types
with meanings like “a function that
takes two numeric arguments and returns a Boolean,” allowing the type checker to verify that
the arguments used in a function call match up with that function’s definition.

Type systems can carry other information too: Java has a
type and effect system
that tracks not only the
types of methods’ arguments and return values but also which
checked exceptions
can be thrown by the body of the
method (throwing an exception is an
effect
), which
is used to ensure that all possible exceptions are either handled or
explicitly propagated.

• Anyone can design and implement a programming language. The basic ideas of syntax and semantics are simple, and tools like Treetop can take care of the uninteresting details.
  

• Every computer program is a mathematical object. Syntactically a program is just a large number; semantically it can represent a mathematical function, or a hierarchical structure which can be manipulated by formal reduction rules. This means that many techniques and results from mathematics, like Kleene’s recursion theorem or Gödel’s incompleteness theorem, can equally be applied to programs.
  

• Computation, which we initially described as just “what a computer does,” has turned out to be something of a force of nature. It’s tempting to think of computation as a sophisticated human invention that can only be performed by specially-designed systems with many complicated parts, but it also shows up in systems that don’t seem complex enough to support it. So computation isn’t a sterile, artificial process that only happens inside a microprocessor, but rather a pervasive phenomenon that crops up in many different places and in many different ways.
  

• Computation is not all-or-nothing. Different machines have different amounts of computational power, giving us a continuum of usefulness: DFAs and NFAs have limited capabilities, DPDAs are more powerful, NPDAs more powerful still, and Turing machines are the most powerful we know of.
  

• Encodings and levels of abstraction are essential to harnessing the power of computation. Computers are machines for maintaining a tower of abstractions, beginning at the very low level of semiconductor physics and rising to the much higher level of multitouch graphical user interfaces. To make computation useful, we need to be able to encode complex ideas from the real world in a simpler form that machines can manipulate, and then be able to decode the results back into a meaningful high-level representation.
  

• There are limits to what computation can do. We don’t know how to build a computer that is fundamentally more capable than a Turing machine, but there are well-defined problems that a Turing machine can’t solve, and a lot of those problems involve discovering information about the programs we write. We can cope with these limitations by learning to make use of vague or incomplete answers to questions about our programs’ behavior.