Jonas is a developer and construKction worker at Computas, with an MSc in Computer Science from the University of Oslo. Codes in new-old languages like Java and Smalltalk at work. Plays with lambdas and programming languages outside of. Almost organizes a lambda-almost-meetup sometimes. Wants to have a goat and a maybe donkey. Donkeys are like small horse-rabbits.
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.