Biblio

The simplest and purest practical object-oriented language designs
today are seen in dynamically-typed languages, such as Smalltalk
and Self. Static types, however, have potential benefits for productivity,
security, and reasoning about programs. In this paper, we describe
the design of Wyvern, a statically typed, pure object-oriented
language that attempts to retain much of the simplicity and expressiveness
of these iconic designs.
Our goals lead us to combine pure object-oriented and functional
abstractions in a simple, typed setting. We present a foundational
object-based language that we believe to be as close as
one can get to simple typed lambda calculus while keeping objectorientation.
We show how this foundational language can be translated
to the typed lambda calculus via standard encodings. We then
define a simple extension to this language that introduces classes
and show that classes are no more than sugar for the foundational
object-based language. Our future intention is to demonstrate that
modules and other object-oriented features can be added to our language
as not more than such syntactical extensions while keeping
the object-oriented core as pure as possible.
The design of Wyvern closely follows both historical and modern
ideas about the essence of object-orientation, suggesting a new
way to think about a minimal, practical, typed core language for
objects.

Programming languages often include specialized syntax for common
datatypes (e.g. lists) and some also build in support for specific specialized
datatypes (e.g. regular expressions), but user-defined types must use generalpurpose
syntax. Frustration with this causes developers to use strings, rather than
structured data, with alarming frequency, leading to correctness, performance,
security, and usability issues. Allowing library providers to modularly extend a
language with new syntax could help address these issues. Unfortunately, prior
mechanisms either limit expressiveness or are not safely composable: individually
unambiguous extensions can still cause ambiguities when used together.
We introduce type-specific languages (TSLs): logic associated with a type that
determines how the bodies of generic literals, able to contain arbitrary syntax,
are parsed and elaborated, hygienically. The TSL for a type is invoked only
when a literal appears where a term of that type is expected, guaranteeing noninterference.
We give evidence supporting the applicability of this approach and
formally specify it with a bidirectionally typed elaboration semantics for the
Wyvern programming language.

Breaches of software security affect millions of people, and therefore it is crucial to strive for more secure software systems. However, the effect of programming language design on software security is not easily measured or studied. In the absence of scientific insight, opinions range from those that claim that programming language design has no effect on security of the system, to those that believe that programming language design is the only way to provide “high-assurance software.” In this paper, we discuss how programming language design can impact software security by looking at a specific example: the Wyvern programming language. We report on how the design of the Wyvern programming language leverages security principles, together with hypotheses about how usability impacts security, in order to prevent command injection attacks. Furthermore, we discuss what security principles we considered in Wyvern’s design.