Das wird heiß

Makarius

FizzBuzz, Python und Isabelle

Gepostet am 26. Nov 18 von iblech

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

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

Anschließend plaudert 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.”