Visible to the public A New Kind of Program LogicConflict Detection Enabled


Noddle is building a code synthesis technology called ``pyx''. Pyx is a generic tool that can be specialized to different domains. For a given domain, pyx enables developers to write high-level applications in Python and generate specialized code to run on a range of platforms. Code is generated using an using an infrastructure that combines source-to-source program transformation, inference and automated search to explore the design space of algorithms and representations.

Each instance of pyx is in populated with transformation rules. Rules are written in a conservative extension of Python and collectively encode the semantics of Python, design knowledge for the domain and strategies for mapping abstract code to a specific platform.

Synthesis, like verification, depends on being able to reason about both code and specifications. In the case of Python, that means imperative code. And for pyx, it means being able to discharge proof obligations that appear in transformation rules. We experimented with using conventional logics and Floyd-style annotations for writing specifications. Similarly, we looked at leveraging external tools for inference. In the end we concluded that it was unlikely that such approaches would be accessible to prospective users or lead to effective inference.

Instead we have developed a new kind of program logic. The logic has a surprisingly simple model-theory and proof theory and offers the prospect of being able to reason about code and produce evidence (ie. proofs) using abstractions and syntax that are familiar to developers. Work on a prototype prover for transforming and reasoning about Python is ongoing.

Lindsay Errington is a co-founder at Noddle. He was formerly a member of the the research staff at Kestrel Institute, Galois and Sandia National Labs in Livermore. With a background in logic and semantics of programming languages, he builds tools for developing high-assurance and high-performance applications.

Lindsay Errington
Matthew Sottile