Synquid generates programs from concise, high-level type-based specifications. It's the first synthesizer to automatically discover provably correct implementations of sorting algorithms, as well as balancing and insertion operations on Red-Black Trees and AVL Trees. For these programs, the required specifications are up to seven times more concise than the implementations, and the synthesis times range from fractions of a second (for insertion sort) to under a minute (for Red-Black Tree rotations)
