I believe Felix has a special syntax to combine declaration and initialization (well, more like a shortcut; IIRC they have type inference for those cases). The code sample just shows that if you need to separate declaration and initialization, you can.
I don't know about Felix, but even the simplest C compilers I use are able to warn me when they can't verify that a variable is initialized before first use. It's not that hard. And, no, you don't have to solve the halting problem as long as you're clear what you promise to warn about. There are cases where you can trivially prove initialization or failure to initialize. Promise to get those cases right, and to warn on anything else.
I don't know about Felix, but even the simplest C compilers I use are able to warn me when they can't verify that a variable is initialized before first use. It's not that hard. And, no, you don't have to solve the halting problem as long as you're clear what you promise to warn about. There are cases where you can trivially prove initialization or failure to initialize. Promise to get those cases right, and to warn on anything else.