Elektrine lite

← Feed

@jeremysiek@types.pl

Post #872112

2026-03-05 01:19 UTC

@krismicinski did some experiments with codex today, looks like it can generate many grad level PL theory solutions in Lean.

Replies (2)

  • @csgordon@discuss.systems 2026-03-05 01:42

    @jeremysiek@types.pl @krismicinski@types.pl I'm moving all of my classes to required code walks. Has the nice side effect of the fact that once you convince your students that the code walk grade doesn't suffer when you find a bug during it, it often turns into a design discussion and talking about debugging strategies. I think the students also feel like their hard work is more appreciated after they actually get to chat with faculty about it. Has worked wonderfully in undergrad compilers and grad distributed systems. Hard to scale past 40 students though

    Open ##2575173

  • @jfdm@discuss.systems 2026-03-05 19:15

    @shriramk@mastodon.social @csgordon@discuss.systems @lindsey@recurse.social @jeremysiek@types.pl @krismicinski@types.pl right so to be clear on these things, the doom part is because the actions require not so trivial changes in how we do things. Within UK academia we are under lots of pressures, with not a lot of time, and not the same power and influence as 'full chairs' do in the states. More so, 1. open book assignments do not exclude the use of GenAI, they can embrace it, and you can guard against or incorporate its use. Such assignments, in my experience are harder to design, and require training on how to do well. 2. Exam conditions are also important as we want students to not rely on GenAI, and to ensure they have the fundamentals down. The argument with GenAI is must be how our forefathers thought about pocket calculators...and their forefathers thought about slide rules, and so on.

    Open ##2575180