Large 00018

Implicit Programming

Viktor Kuncak

Recorded 17 November 2011 in Lausanne, Vaud, Switzerland

Event: KTN - Know Thy Neighbor

Abstract

Programming is harder than it should be. To make it easier, we propose implicit programming, a declarative programming model where automated reasoning plays a key role during: (1) interactive program development; (2) program compilation; and (3) program execution.

For each of these aspects of software development we present an implemented tool that advances it. For interactive development we present synthesis based on type constraints, running within a program editor. For program compilation, we present synthesis procedures that compile desired properties into explicit executable code. For program execution, we present a system that performs constraint solving and solution enumeration at run time, increasing the expressive power of programs, supporting test case generation, prototyping, and the use of contracts as safety nets.

Key insights behind our tools are new theorem proving and constraint solving algorithms for infinite domains, such as algebraic data types with recursive functions, multisets, and sets. Our work builds on the Scala language infrastructure, including its tool support and the capabilities for domain-specific language embedding. In the future we plan to extend and leverage this technology to empower broader segments of the population to develop and customize our computational infrastructure.

Watched 16627 times.

 Watch