Both - or none.
It depends upon how good the design is verified, not how it is implemented. An µC programmed in Ada by a trained person is very reliable (military-grade). An µC programmed in Assembler is not reliable. C99 or even C++ is better provided that you have a skilled developer (it's virtually impossible to find a C++ one) but still not as good as Ada.
A Verilog or VHDL FPGA design is somewhere between C99 and Ada. It is quite easy to verify. On the other side, it would be probably larger which makes it harder to maintain (and increases the probability of verifying it incorrectly.
Do not trust tests. Only a formal proof guarantees that your product works well. A formal proof is easily doable in Ada, VHDL or Verilog, a bit harder in C99 and good C++11 code. It is hardly possible in poorly-written C++ or C89 code.
May we get an example of such proof in those languages? Because formal proof isn't something people talk about often, so most of us are not familiar with this.
Also, if we want to program in Ada, which mcu development environment allow Ada programming? (I am not talking about compiling my own gcc tool-chain with ada enable)
You don't need to program in Ada to be able to prove program correctness - i.e. that a program execution stops (doesn't run in an endless loop forever, never returning an answer) and that the answer returned is actually correct. Both of these have to be true for a program to be considered
totally correct (otherwise it is only
partially correct). Special cases, such as MCU code running forever are a trivial extension - each iteration of the main loop has to be correct.
You can even formally verify assembler if you want (so no, there is nothing inherently "unreliable" about assembler - let's not talk long term maintenance issues). Formal verification has nothing whatsoever with the choice of a programming language, however, some languages do make things easier (or more difficult).
One example of a formal method that is still used and is targeting structured program schemes - i.e. languages similar to Pascal, C, Java, C++, etc. that use nested high level control blocks (unlike e.g. Fortran, Basic or that assembler) is Hoare method. From a very high level point of view, Hoare method is basically a mathematical induction over the program blocks. If I prove that all sub blocks are correct and are correctly linked together using pre and post conditions, then I can conclude that my current block is correct as well. You continue doing this until you arrive to the top-level block of your program (e.g. you main() function).
I am not going to do a proof here, that would be too long, but you can find an example of this here:
http://www.cs.cmu.edu/~aldrich/courses/654-sp07/slides/7-hoare.pdf and here:
http://www.slidefinder.net/h/hoare_method_proving_correctness_programs/c21_hoare/15496132Now Hoare method proves only partial correctness - that is, the result is going to be correct,
if the program stops. It does not guarantee that the program actually stops - that you have to prove separately.
Now, if you want to prove correctness of something like assembler code or Basic/Fortran, you can use Floyd's method instead. A quick introduction is here (yes, the techniques are THAT old - 1967, Hoare 1969 ...):
https://users.cs.duke.edu/~raw/cps206/ProgramCorrectness.htm It is more laborious and you have to set good invariants, otherwise your proof will not be good for much.
Both of these two methods can be greatly helped if your programming language has some special features. E.g. if you are doing design by contract like in Ada you are going to have much easier time proving your program correct, because you can rely on this language feature.
Another thing are side effects - if your functions are side effects free (aka pure - their result depending only on their arguments and not anything else and they are not modifying anything else), then the proof is going to be much easier. Complicated side effects where behaviour of a function could depend on things outside of it (and thus not covered by pre/post conditions or invariants) could make the proof very difficult or impossible. This is one reason why functional programming is so popular among theoretical computer scientists - functional programming deals only with pure functions, so the problem with side effects is eliminated. Now that has some practical consequences because a real program needs at least some side effects - such as I/O - and there are some complex theoretical frameworks dealing with these (e.g. monads in Haskell).
A final remark - FYI, the neither Space Shuttle nor the Apollo guidance computer code were formally verified (there weren't computers powerful enough to do the verification in a reasonable time available). However, they very employing some very good software engineering practices. So that could be worth more than trying to go into formal verification which is extremely hard for anything but trivial programs.