I started developing Aeon back in 2018 as a playground for program synthesis. Holes (?x) are valid expression in aeon (def f (i:Int) : Int := i * 2 + ?x compiles successfully and, when ?x is evaluated at runtime, it opens a repl asking the user for the right expression). However, the main advantage of holes is when you run the aeon compiler with "--synthesizer", it tries to find a suitable expression for the holes in your program. This blog post covers the different methods you have to describe what you want a function to do. We've decided on the function-level for the specification as it is the most normal public (and private) API of your code.
Basic Types
Aeon is a (very strongly) typed language, so you always need to write the types of top-level functions.1 As such, all proposed candidate expressions to replace ?hole need to type-check. So writing Int as the return type already specifies something about the missing code.
def double (x:Int) : Int := ?hole
Liquid Types
Aeon supports liquid types by refining a basic type with a predicate. In the case below we refine the returning type of the function Int with the predicate that it needs to be equal to twice the value of x. Because Liquid Types can refer to other values in the program (such as function arguments), they are (value-)dependent types, but following a different discipline than the (full) dependent types you find in Lean, Rocq or Idris.
def double (x:Int) : {r:Int | r == x + x} := ?hole
So far, this definition covers both Refinement Types and Liquid Types. The main distinction of the two is that the refinements in Liquid Types need to be drawn from a decidable logic, so an SMT solver can give you a definitive answer of whether it type checks or not.
Liquid types guide synthesis directly in approaches such as Synquid and Liquid Tree Automata. In Aeon, their logical predicates can also be translated into constraints for SMT solving with Z3, syntax-guided synthesis (SyGuS), polynomial synthesis, and OR-Tools’ CP-SAT solver. Liquid Types are also used in our own custom synthesis algorithms that combine evolutionary search and liquid types.
Natural language documentation
Aeon also supports AeonDoc, using the @doc decorator to annotate a natural-language description of the function. We can take this documentation as input to a synthesis method (currently, only LLM-based synthesizers support @doc). This documentation complements any type that constrains the hole already.
@doc("Doubles the input.")
def double (x:Int) : Int := ?hole
Examples or test cases.
Aeon supports the decorator @example that takes a boolean predicate about the execution of the final synthesized function.
@example(double 3 = 6)
@example(double 5 = 10)
def double (x:Int) : Int := ?hole
Input–output examples guide many synthesis approaches: automata-based methods such as AFTA use them to prune spaces of candidate programs; top-down methods such as Myth or Decision Trees propagate examples into smaller synthesis subproblems; and bottom-up methods such as BUSTLE compose programs from smaller expressions evaluated on those examples. Examples also define fitness functions for genetic programming and provide training data for decision-tree learning, which learns conditional rules mapping inputs to outputs.
Decision Trees and Genetic Programming, coming from the Machine Learning backgrounds, assume that some examples might be wrong so they are more permissive. Other methods typically search for a solution that covers all examples. In this case, only noise-supporting methods can handle contradictory examples.
Because writing examples can be tedious, you can use CSV data directly or through an auxiliary file (@csv_data("1.0,2.0\n3.0,6.0\n4.0,8.0") or @csv_file("double.csv").
Optimization goals
@minimize_int(abs $ (double 4) - (4 * 2))
@minimize_int(abs $ (double 5) - (5 * 2))
def double (x:Int) : {r:Int | r = x + x} := ?hole
Aeon supports multiple maximize and minimize decorators to express optimization goals. We might know a given ideal target for the minimization criteria or not (for open problems). This example is the former, where you cannot have a value lower than 0. However, if you were to maximize the return value of a function that returns prime numbers, you would have no target value.
When multiple objectives are set, we consider this a multi-objective optimization problem and each algorithm typically returns the Pareto set, containing solutions that no other candidate is better in all axis. Genetic Programming and OR-Tools solvers have these features built-in. Recent Genetic Programming approaches have recommended Lexicase-selection instead of a Pareto tournament, but my own experience does not confirm this recommendation. If you are going to evaluate all objectives, then lexicase selection might make sense, but because tournaments only evaluate one objective for few good candidates, it ends up being more computational cheaper, and more time is left for exploration.
A big advantage of examples and optimization constraints over liquid types is that you can write any aeon expression that you want (such as multiplication of variables i*j). Because Liquid Types are limited to decidable theories, you cannot write2 this multiplication and other types of expressions and you are limited to linear integer arithmetic, arrays, uninterpreted functions and other SMT theories.
Property-based Tests
Property-based testing is the idea that instead of writing concrete input and output examples, you write properties that relate them, and have random inputs generated to validate those properties. For me, it is very similar, if not the same, as Metamorphic testing.
def double (x:Int) : Int := ?hole
@property(100)
def prop_double_is_bigger (x:Int | x > 0) : Bool := double x > x
In this example, the body of the double function will have to work with 100 randomly-generated inputs and return a value that complies with the state property every single time.
Results
You can either run aeon on the command line, selecting the synthesizer method with -s (python -m aeon multi_objective.ae -s gp --budget 10), or use an LSP editor to ask the compiler to synthesize using a particular method. If you are using VSCode, you have an extra interface to explore program synthesis.
The first specification yielded def double (x:Int) : Int := 1, which matches exactly what we asked it to return: an Integer. When using the other specifications we got a variety of solutions: x+x, 2*x and x+x+0. But this is with a very simple specification that I would assume any synthesizer should be able to generate. Larger examples are left to the reader (or to the next blog post).
Non-functional requirements
All of the intent that we have expressed for far was related to functional correctness. But software developers know that non-functional properties can be equally important in some projects. As such, we are adding support for different forms of expressing quality properties. In particular, we already support @minimize_cputime(expression) and @minimize_energy(expression) for minimizing execution time and energy consumption respectively. Despite this support, the example above is too simple and trivial that the measurement overhead is many times that of the execution. I would only recommend using these advanced decorators for larger programs.
And aeon also supports other properties, you just need to write the code that translates the candidate function into a measure of that quality, using the example or optimization decorators.
Happy synthesizing!
-
This restriction comes from Liquid Types. ↩
-
Actually you can, but you will get a warning. This is an UX improvement we are making based on our paper on challenges of Liquid Types adoption. ↩
