How to express intent in aeon

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…

Commenting on Bubbles has been removed. Why? If you want to talk about this post, write to the author, use the comments on their blog if it has them, or reply with a "RE:" post on your own blog. Suggestions? feedback@bubbles.town