True, I didn't say the solution was perfect, but it is good enough for most devs.
> You raise the craftsman to the level the craft requires, not lower the craft to the level of an apprentice.
Nice goal, but I doubt you would manage to achieve that to anyone doing enterprise CRUD apps, mobile apps, games, ... to bother one second to learn TLA+, Idris, Coq or similar, unless their jobs depend on it.
> As I said before, resource management is first and foremost a matter of correctness, so performance is neither here nor there.
Your proposed alternatives, namely:
> In Modula-3 or D, as possible examples, a solution might be destructors or scope attributes.
merely offer automation, not verification. Automation without verification simply makes screw-ups harder to undo.
These still allow you to mismanage resources.
> The only way to actually be 100% safe would be if everyone would be programming with formal logic,
Indeed. In order to construct a correct program, you also need to construct the logical argument that establishes its correctness. So, yes, you have to use formal logic.
> which still requires a lot of research to make it approachable by the average developer.
s/research/education/
You raise the craftsman to the level the craft requires, not lower the craft to the level of an apprentice.