I work on software for a product used mainly on fighter jets. I just fell into the industry.
The main barrier to entry is to know C. I don't mean that you've written a few basic programs in it, or had a one semester class with it. You need to know C front and back. Be able to identify undefined behavior, complete large programs unsupervised. Several people I work with keep copies of the ISO standard at their desk.
Most of the people I work with have an education in computer engineering, but my background is in CS and math.
Embedded programming isn't really difficult as long as you're using it appropriately. I wouldn't want to use a micro-controller to do a bunch of heavy math, but they're easy to work with basic peripherals that communicate over I2C and SPI. It's actually fairly fun to work on that stuff.
As far as your dream of working on software checked for correctness. I don't know what industry that would be. Military software doesn't have to meet the requirements set by the FAA (civilian stuff). Most do require you to code "towards" DO-178, but there's no CA.
MISRA and JPL guidelines are things that can mostly be checked by PC-Lint and the like. They will help you catch corner cases of writing bad C code. They won't make the code correct.
DO-178 tends to remind me of ISO-9001. They do mandate a few programming practices, but largely you write a set of documents about how you intend to write software, and you make sure you produce artifacts showing you followed your procedures. It doesn't actually verify the correctness of code.
The one thing that I have been amazed about is traceability. It's the one thing mandated by DO-178 that appears to work, and work incredibly well. I think more than any other aspect it traceability explains the excellent track record of avionics software.
We of course do everything we can to make sure the code is correct. I think more than anything, working in this industry creates a company culture of safety. That culture allows for schedules with a proper chunk of time put in for making sure the software is quality.
My advice for getting into the industry would be to learn C really well. Demonstrably well. Grab an dev board for a micro and do a basic project. Then apply to jobs at all the major defense industry contractors. You might not be working on aerospace the first few years, but it'll be a stepping stone to getting your foot in the door.
I'd suggest reading a book on writing safety-critical software before you go too far. Just to make sure it's something you really want to do. I think you'll find the book spends much more time explaining how to write required CYA documents than it does giving you advice on how to write highly-reliable software.