Rehabilitating the POSIX shell
We build intricate systems with complex algorithms and invariants,
aiming for guarantees of correctness and performance… and then we
maintain and deploy these systems with shell scripts! What *are* shell
scripts? If the POSIX shell is a programming language, what are its
syntax and semantics? Can we apply PL tools to reason about the shell?
Why haven’t prior PL attempts at understanding the shell redeemed it?
In this talk, I’ll explain the shell’s semantics, demonstrate a tool
for understanding the shell built on a mechanized small-step semantics
of the shell, and explain why my approach is different from prior
academic work on the shell.
Michael Greenberg is an assistant professor at Pomona College. He
received his BA in Computer Science and Egyptology from Brown
University (2007) and his PhD in Computer Science from the University
of Pennsylvania (2013). His work has ranged from functional-reactive
verification of higher-order programs using contracts (with Benjamin
Pierce at Penn) to software-defined networking (with Dave Walker at
Princeton) to present activities focused on Kleene algebra with tests
and the POSIX shell.