@krismicinski did some experiments with codex today, looks like it can generate many grad level PL theory solutions in Lean.
Remote
Jeremy
@jeremysiek@types.pl
mastodon 4.8.0-alpha.2+glitchJeremy Siek is a Professor at Indiana University where he teaches courses about algorithms, compilers, and programming language theory. Jeremy authored the book ``The Boost Graph Library'' and designed constrained templates for C++, aka the "concepts" proposal. Jeremy invented gradual typing: a type system that integrates both dynamic and static typing in the same programming language.
619 Followers
60 Following
12 Posts
Joined November 08, 2022
Codex and GPT 5.3-codex are blowing my mind... accelerating proof development and refactoring in Agda for programming language metatheory. Lots of grunt work is becoming automatic, but regular guidance is still needed.
The ACLU of Indiana has filed a lawsuit against Governor Mike Braun over the law that changes how members of the Indiana University Board of Trustees are selected.
https://www.aclu-in.org/en/press-releases/aclu-indiana-sues-governor-braun-over-sections-hea-1001-target-indiana-university
Over 260 faculty, staff urge IU to undo Xiaofeng Wang’s termination
https://www.idsnews.com/article/2025/05/faculty-staff-letter-to-provost-xiaofeng-wang-tenure-termination
Verified Nanopasses for Compiling Conditionals
@krismicinski which class?
Replying to