I think the reason we argue about this constantly is that we treat this like a 1 dimensional problem when it's the classical 2 dimensional problem where 3 quadrants are tenable and people only agree that there is a bad quadrant, an ideal quadrant, and then we argue endlessly about the remaining two.

The truth is probably that the value of verifying correctness at compile time is proportional to how often the code will be run. There is space for 'glue' code that is in a simpler language, as long as we relentlessly search for code that deserves to be promoted to a more robust representation.

Take game engines for example, where story-driven elements are driven by a scripting language, often Lua, for decades now. The real engine is in a language the narrators probably can't understand, which affords the engine designers the right to change their minds about how it actually works.

I think we expect firmware and silicon to be run millions of times more than any particular piece of code. So the question is "Why Python for this scenario?" and I'd like to know the answer too.