I often see these precise points in code review arguments, by developers doing something 'risky' in their code: "It's only risky if you don't know what you're doing."
Half the time the same developer has made a mistake in the same code.
With software being so complex, so full of human error -- almost any tool and practice that can help remedy this situation is welcome in my books.
I think it's entirely reasonable to write security-focused software in a highly restricted language with concrete formal semantics.
The problem with trivial examples is that they're often constructed to prove a point and don't represent what a real developer would write if they were to seriously consider the problem in C.
