It's very impressive that the synthesizer came up with that instruction sequence. The technique used is too slow for general compiler optimization (tens of seconds to an hour for short programs) but useful for specialist problems.

This is worth trying on bit-pushing algorithms such as crypto and compression algorithms. Those use so much CPU time that the effort is justified. It might also be useful for generating code that uses MMX/SSE2/3/4 instructions.

> Of course, at some level this isn’t very different from what compilers have been doing for ages, if we consider the source language program to be the specification, but when we’re doing synthesis the connotation is that the specification isn’t directly implementable using standard compiler techniques.

I guess compiling lazy functional languages was synthesis at one point, too, before people really figured out how to do that efficiently via eg the tagless spineless g-machine.

I wonder whether synthesis is like AI: whenever we understand how to do something, like play chess, it's no longer AI.

EDIT: Comments on the site delve into that very topic.

Cool! And somewhat scary, shifting the work of the human to verify and understand machine-generated code.

Also, obligatory nitpick: the example naive C implementation uses bitwise AND (&) when it means boolean AND (&&), the line that starts:

    return
        (n00 == n01) & (n00 == n02)

This is bad, since bitwise AND in C isn't short-circuiting. It's also bad since it's semantically weird, the things being AND:ed are obviously truth values (the results of lots of == operators), which are not necessarily the same as "raw" bits.

In C, == simply produces a numeric value (0 or 1). There's nothing "weird" about the subsequent operation of & on those values.

There's no effects to make short-circuiting a problem, either - on the contrary, it is likely that the programmer had branchless code in mind.

Blush.

You're right, at least in that == produces 0 or 1. I was sure it had been "ported" to produce _Bool when that was added (which then of course automatically converts to 0 or 1 as needed), but that seems not to be the case.

I still think the ANDs should be boolean (i.e. &&) though, but perhaps your hunch about branchlessness is right.

Thanks.

Can I get a less intense summary?

Say you have a list of full names and you want to teach a computer to get the first name out of each.

With "program synthesis", you provide a couple example outputs, and the computer tries to generate ("synthesize") a program that turns the input (i.e., the full name) into the output (i.e., just the first name).

Basically, this works as follows. You generate a ton of candidate programs, and then rank them that work for the input, and choose the "best" among them, and return that. The ranking is a bit of an art though.

"you can make computers do things you have to think about to understand."

or maybe even "you can get computers to figure things out, and it's cool when the computer reasons something in a way you hadn't thought of"