Tracking issue for records
@tchajed, @robbertkrebbers and me are discussing ideas for equipping Iris with support for "named records", based on a first implementation of sch a scheme by Tej for Perennial. This is a tracking issue where we track which pieces of work depend on what, and what needs to be done next.
The current status is that some unforeseen issues came up after merging !479 (merged), but we'd rather not change the naming system until we have a way to reliably control the names used for existentials in a record. Record design itself is blocked on some fundamental questions.