Refine yourself a code for great good!#
Abstract#
How do you code? Andrej Karpathy who coined the term “vibe coding,” says that for professional coding tasks, he picks single concrete incremental changes and, with AI assistance, plans them, executes them, and evaluates them. Refinement is the process of making incremental changes. It is not just the primary way we design and construct code, but also how we repair them and upgrade them, often collaboratively with other coders, designers and users.
The central objects in refinement are partially implemented programs. Partial programs are examples of open systems - each has a formal external specification (e.g. a function type) and an implementation with internal holes which are also formally specified. Partial proofs, such as those manipulated by the proof assistants, are also examples of open systems. Open systems compose by refinement or hole-filling, where a typed hole can only be filled by an open system of the right spec. An open system in some representation can also be translated (transported, projected or lifted) to some open system in another representation. In fact, open systems, with their refinements and translations, form a double category!
In this talk, I hope to share some concrete examples of this refinement-centric approach in formal verification, program synthesis and theorem proving. I believe that this approach can help us to leverage AI assistance in coding, to decentralize and democratize coding, and to build safe, secure and sustainable software systems.