Not GP, but something generated by CoPilot (https://hackage.haskell.org/package/copilot) would generate constant-time constant-memory C code from a specification written in a DSL. That is what I would start to consider "proper" safe for stuff where it is really important.
It depends on what you consider to be absolute requirements for proper concurrency safety of course, and how much of the hardware is allowed to fail before it starts impacting the software.
It depends on what you consider to be absolute requirements for proper concurrency safety of course, and how much of the hardware is allowed to fail before it starts impacting the software.