Start adding safety flags and removing naughty bits

[dsheets]

trafficstars

Holes, non-termination, and postulates, I'm coming for you. Switching to coinductive records for composability between coalgebras.

[jmlowenthal]

Looking good! FYI I've been looking at an implementation of CMinor as a replacement of this limited and faulty(ish) C Lang

[dsheets]

I'm looking at the postulates in https://github.com/jmlowenthal/agda-c/blob/master/src/C/Semantics/SmallStep/Properties/Program/Equivalence.agda and hitting some issues with the representation of language constructs and semantic reductions. What is the reason that these types are records rather than, say, inductive families? Extensibility? Multiple interpretations? Are there any inhabitants of these types around? What enforces the inhabitability of these types?

Thanks :-)

[jmlowenthal]

Multiple interpretations is the main goal here, which can be rather problematic in places and has been the source of bugs. Here is an example implementation of Lang, but I don't think there are any implementations of Semantics hanging around.