> As an Arduino enthusiast I see statically allocated (global?) variables are frequently the way to go for an embedded system, the frontier is to be able to prove the correctness of what you're doing.

As a professional in the embedded and safety critical systems space: No, they aren't "the way to go". You often end up with a small number (think "singletons" for OO people) but the rest can be done properly with local variables or more limited scope variables instead of garbage global variables to manage complex system state.