A Formally Verified Interpreter for a Shell-Like Programming Language

[lainon]

https://hal-univ-diderot.archives-ouvertes.fr/hal-01534747/document

[chubot]

FWIW I posted just posted a comment on lobste.rs with a preliminary comparison to my project, http://www.oilshell.org .

https://lobste.rs/s/fi6lax/formally_verified_interpreter_for...

In short there are a bunch of similarities and similar engineering work as far as I can tell, but I'm not done reading the paper.

The paper is from this summer, but I didn't know about it until nickpsecurity posted it today! Hat tip to him.