[yannickmoy]

You can get automatic resource handling with controlled types, but this is not part of the baremetal minimal runtime you can use for a driver.

You can get ownership tracking with SPARK, but you need to use proof techniques.

There are pointers in Ada, but it's not at all the same as in C. First, C pointers are really addresses, references and pointers in Ada. And pointers come in various flavors named/anonymous access-to-variable/constant/subprogram, pointing only to the heap or also to the stack, with accessibility levels depending on where the type is defined... which lead to fine-grain distinction of the various use cases with SPARK so that only correct use is provable.