Msh log 2026-38 [msh-log-2026-w38]

After running some Dockerfile analysis last week, I have focused on formalising some operational semantics for the core POSIX-shell inspired language for a "mergeable shell".

This work borrows from Smoosh, but extends the semantics to include reasoning about namespaces, filesystems and effects.

For instance, here are two inference rules for field splitting and parameter substitution. Here, \sigma tracks the shell state, \phi is the filesystem and \tau tracks the side effects.

There are lots of interesting examples of this, like assignment during parameter substitution (e.g. ${FOO:=BAR}) or the side effects that take place during program name resolution.