Implicit programming is a proposed software development paradigm that aims to address longstanding bottlenecks of software construction. The problem that we address is obvious to anyone who has ever written a program: programming is harder than it should be. Although programming activities include some seemingly unavoidable aspects, such as describing the goal of the computation and certain creative aspects of its solution, most of it is tedious and low level. It requires explicitly spelling out and elaborating conceptually simple steps, and ends up requiring more effort than one initially expects. As a result, even easy tasks require the work of professionals and experts, whose programming skills are in stark contrast to the remaining users of computing infrastructure. In the decade with billions of users of computing resources, blurring this contrast can have far-reaching economic and social consequences. Our implicit programming paradigm aims to blur this divide by making software construction substantially easier at several levels, from new declarative programming language constructs to new software development tools. We support implicit programming with a new concept of synthesis procedures, which enhance algorithms in today's compilers by building on the advances in satisfiability modulo theories (SMT) and the rapidly expanding field of software synthesis. We aim to deploy our algorithms through new run-time platforms that perform program analysis and optimization to support and leverage synthesis procedures in the context of the overall application. Finally, we are introducing new development tools, application manipulation interfaces, and techniques to handle ambiguity, making development easier for both experts and non-experts.

Your wish is my command

Videos:

• RV Keynote: Executing Specifications using Synthesis and Constraint Solving
• Synthesis in Leon
• Brick Breaker in Pong Designer - version from 2012
• Viktor's Inaugural Lecture at EPFL (uses flash)
• Verification in Leon

The following are some of the related papers that explore these techniques and tools and describe our results so far:

• Software Synthesis Procedures (CACM 2012)
• Functional Synthesis for Linear Arithmetic and Sets (STTT 2012)
• Constraints as Control (POPL 2012)
• Synthesis for Unbounded Bitvector Arithmetic (IJCAR 2012)
• Complete Functional Synthesis (PLDI 2010)
• Synthesis of Regular Specifications over Unbounded Domains (FMCAD 2010)
• Test Generation through Programming in UDITA (ICSE 2010)
• Simplifying Distributed System Development (HotOS)

General talks about these topics were given at several keynotes, lectures, and summaries. Here are a few versions of these talks:

• Overview for EPFL Doctoral Students, September 2011
• Dagstuhl, August 2011 summer school: Lecture 1,Lecture 2
• BoogiePL keynote: August 2011, Wroclaw, PL
• SMT keynote: July 2011, Snowbird, USA. Here is the abstract
• Verimag seminar talk: May 2011, Grenoble, FR
• PUMA talk: February 2011, Munich, DE

The starting point for implicit programming is our recent work on complete functional synthesis and regular synthesis for unbounded domains, interactive synthesis using resolution-based techniques, work on test generation, as well as our work on decision procedures.

Currently available tools that explore aspects of implicit programming are:

• Comfusy - Complete Functional Synthesis
• Kaplan - Programming with First-class Constraints
• Pong Designer - Programming Games by Demonstration
• RegSy - Regular Synthesis over Unbounded Domains
• Interactive Synthesis
• UDITA Tool for Systematic Test Generation
• Scala^Z3

Funding acknowledgement: This project is supported by the European Research Council (ERC) Starting Grant awarded to Viktor Kuncak, who leads the Lab for Automated Reasoning and Analysis at EPFL.