|
Ko, Andrew
|
SPLASH Companion '16-KEY: "A Human View of Programming ..."
A Human View of Programming Languages (Keynote)
Andrew Ko
(University of Washington, USA)
In computer science, we usually take a technical view of programming languages, defining them as precise, formal ways of specifying a computer behavior. This view shapes much of the research and development that we do on programming languages, determining the questions we ask about them, the improvements we make to them, and how we teach people to use them. But to many people (even software engineers) programming languages are not purely technical things, but socio-technical things. In this talk, I discuss several alternative views of programming languages, and how these views can reshape how we design, evolve, and use programming languages in research and practice.
@InProceedings{SPLASH Companion16p2,
author = {Andrew Ko},
title = {A Human View of Programming Languages (Keynote)},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {2--2},
doi = {},
year = {2016},
}
|
|
Pierce, Benjamin C.
|
SPLASH Companion '16-KEY: "The Science of Deep Specification ..."
The Science of Deep Specification (Keynote)
Benjamin C. Pierce
(University of Pennsylvania, USA)
Abstraction and modularity underlie all successful hardware and software systems: We build complex artifacts by decomposing them into parts that can be understood separately. Modular decomposition depends crucially on the artful choice of interfaces between pieces. As these interfaces become more expressive, we think of them as specifications of components or layers. Rich specifications based on formal logic are little used in industry today, but a practical platform for working with them could signicantly reduce the costs of system implementation and evolution by identifying vulnerabilities, helping programmers understand the behavior of new components, facilitating rigorous change-impact analysis, and supporting maintainable machine-checked verication that components are correct and fit together correctly.
Recently, research in the area has begun to focus on a particularly rich class of specifications, which might be called deep specifications. Deep specifications are rich (describing complex component behaviors in detail); two-sided (connected to both implementations and clients); formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs); and live (connected directly to the source code of implementations via machine-checkable proofs or property-based random testing). These requirements impose strong functional correctness conditions on individual components and permit them to be connected together with rigorous composition theorems.
This talk presents the key features of deep specifications, surveys recent achievements and ongoing efforts in the research community (in particular, work at Penn, Princeton, Yale, and MIT on formalizing a rich interconnected collection of deep specifications for critical system software components), and argues that the time is ripe for an intensive effort in this area, involving both academia and industry and integrating research, education, and community building. The ultimate goal is to provide rigorously checked proofs about much larger artifacts than are feasible today, based on decomposition of proof effort across components with deep specifications.
@InProceedings{SPLASH Companion16p1,
author = {Benjamin C. Pierce},
title = {The Science of Deep Specification (Keynote)},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {1--1},
doi = {},
year = {2016},
}
|