> In Modula-3 or D, as as possible examples, a solution might be destructors or scope attributes.

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.