Die Knoblauchmate-Wikiseite ist jetzt auch mit Tschunk geupdatet :3 #hip5 @nzbr

https://wiki.das-labor.org/w/Rezept:_Knoblauchmate

Yesterday at #hip5 I held a workshop about #agda.

My goal was to try explaining the basics of how theorem proving works and why it's analogous to programming (the Curry-Howard correspondence) to people with a background in programming, but no prior knowledge in theorem proving or functional programming. I hope that that maybe showed an interesting approach to theoretical computer science etc. to some people that previously avoided it.

I think that it least somewhat worked and got positive feedback, which is great :D I'll definitely hold this or a similar workshop again some time.

(the code is at https://git.eisfunke.com/lab/proof-assistants)