[Iris-Club] Iris proof mode artifact ideas for proof automation class

[Talia Ringer]

Hi all,

I'm teaching a class on proof automation
<https://dependenttyp.es/classes/598sp2022.html> this spring. The way the
course works is by alternating between reading discussions and artifact
hacking sessions, where the artifacts are typically derived directly from
the readings. Those sessions are in person, in groups, with a discussion
following the hacking.

One of the readings is the Iris proof mode paper
<https://dependenttyp.es/classes/readings/7-logics.html>. For the artifact
that Thursday, I'd like to make an exercise derived from the Iris proof
mode artifact. I've had no trouble installing the development version from
source (yay), so now it's time to make the actual assignment for the
hacking session.

I'm curious if any of you have ideas for that. Typically these session
include diving into the source of an artifact, looking at some mix of 1)
user experience for the tool, and 2) how the tool is actually implemented.
Ideally this also includes modifying some code to implement some small and
simple extension to the tool, though this isn't always possible.

Goals for the Iris proof mode artifact assignment are *any nonempty subset *of
these goals:
1) get a sense of how the Iris proof mode is implemented, and how one could
implement something similar for another domain or logic,
2) get a sense of how reflection works, and its costs and benefits,
3) get a sense of how language design and automation feed into one another,
and what design decisions make the Iris proof mode possible,
4) get a sense of how type classes work, and whether they impact
scalability.

I'm also open to other goals you all find interesting, though. This is a
brand new class I'm designing from scratch, and I'm very open.

The assignment itself isn't graded, just the discussion question after, so
it's also fine if it's something that can't be finished in one class,
though it's ideal if there's some intermediate progress.

I figured I'd ask the Iris experts if you all have any ideas. Please let me
know if you do!

Thanks,

Talia
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20220113/698faefa/attachment.html>