And for the last of my selection from Strange Loop 2015, here is "Propositions as Types" by Philip Wadler, based on my paper of the same name, which I am told will soon appear in Communications of the ACM. I received more compliments on this talk than for any other, which I take as one benefit of the friendliness and fun of the Strange Loop crowd. Thanks to Alex Miller and the crew for assembling a great conference!