For safety stuff I've worked on, the source had to be vetted, and then someone goes through line by line and confirms that the assembly generated for each line of code matches the source code. For C or Ada with conservative optimizations, this is fairly mechanical (and extremely boring), but means that trusting the compiler is not a requirement.