Einar W. Høst is a computer at NRK, the Norwegian public broadcaster. He thinks that programs should be written for people to read and also for machines to laugh at. He has a PhD in Computer Science from the University of Oslo.
What do we know about logic and programming? Well not much perhaps, but we do know that logic is terribly hard (and proving things is even harder), whereas you can teach yourself C in 24 hours. And so it would be useful if there were some correspondence between logic and programming, because then we could do the easy thing instead of the hard thing! Ha ha! And lo and behold! There is! By magic, luck or the nature of the universe, there is a deep corresporphism between the two, that we will explore in this talk. Which is to say we'll write programs that produce walls of unintelligible symbols as proofs.