Research Project
Dr. Solar-Lezama and his colleagues have been working on a language called sketch for several years. Sketch is a C-like language that is capable of filling intentionally-left holes in a program and reasoning a solution given a unit test or an equivalent implementation. Sketch is very useful for solving difficult programming problems such as thread safety and optimal data structure implementation.
My work this Summer involves adding features to Sketch that allow it to reason about larger pieces of code and allow the programmer to easily define equivalent implementations of larger structures using a unique object-system. This system introduces a new structure in sketch known as a package. Package are similar to conventional object-oriented classes and namespaces in languages like C++. Packages are used to encapsulate functions, variables, and structures. Packages can have parents through a unique inheritance system. A defining aspect of Sketch packages lies in the enforcement of the Liskov Substitution Principle (LSP) for parent-children
Packages can be easily used to describe different implementations of equivalent data structures. One may envision having a SimpleSet which is based on a flat array; this is super simple to implement at the cost of reduced performance. The programmer may also choose to implement a HashSet which is a child of SimpleSet; this may be implemented with holes as SimpleSet is an equivalent implementation. It should be noted that everything in the SimpleSet public API is also in the HashSet public API, the HashSet public API may however be extended with more functions and structs. The compiler, upon analysis/reasoning, may choose the SimpleSet for analysis (since it is much easier to analyze) while using HashSet for the true implementation. The compiler also verifies that SimpleSet and HashSet, as used in the program offer identical functionality.