You're viewing the discuss.systems public feed.

Lars Hupel :verified:lars@hupel.info
Sep 24, 2026, 7:30 AM
@yforster @lindsey I took Tobias' semantics class. I'm not sure either he said that (doesn't sound like him tbh) but anyway it is Correct
he did frequently compare proof assistants to video games, though
💬 1🔄 0⭐ 0

Replies

terrustuebinm@pleroma.stuebinm.eu
Sep 24, 2026, 9:25 AM
@lars @yforster @lindsey i definitely remember him saying a slight variation, as in "this course uses a proof assistant, which is at the beginning harder but can also be addicting" (but i can't remember the exact wording)

i *think* recordings of the semantics course can be found online tho, so it should be possible to check …
💬 0🔄 0⭐ 0
Lars Hupel :verified:lars@hupel.info
Sep 24, 2026, 9:28 AM
@stuebinm @lindsey @yforster yup that sounds more like it
💬 1🔄 0⭐ 0
terrustuebinm@pleroma.stuebinm.eu
Sep 24, 2026, 11:08 AM
@lars @lindsey @yforster ah here they are: https://live.rbg.tum.de/course/2022/W/Sem

(tho at a quick glance i didn't find anything fitting, but also don't have the time to search through it thoroughly)
💬 0🔄 0⭐ 0