FizzBuzz, Python und Isabelle

Das 45. Treffen begann nicht wie üblich um 19:00 Uhr, sondern etwas später um 20:25 Uhr. Als inoffizielles Warmup hielt ein Vortrag in der Reihe Faszination Mathematik/Physik her.

Cornelius implementierte FizzBuzz in Python. “Ich möchte nicht spoilern, aber ich kann bereits verraten, dass das Ergebnis in Isabelle/HOL nicht einmal typcheckt.”

Anschließend plauderte Makarius über das neue Isabelle/Haskell/PIDE mit Anwendung auf “Automatic Checking of Ordinary Mathematical Texts” (Prof. Peter Koepke, Uni. Bonn). “Das ist zwar erst halb fertig, aber zeigen kann man schon was – vor allem auch das ‘Tooling’ für Haskell: ‘Stack’ und VSCode mit Haskell Language Server. Das füllt locker viele GB RAM + HD, aber dafür muss man selber nichts herumbasteln.”