Surprising that dependent types have become mainstream enough for such a conference, or surprising that the computer can write whole paragraphs of code for you if the types are expressive enough? :)