A lot of "High Performance Computing" HPC codes are written in languages like C++, C, sometimes even JAVA or Python simply because the compilers are pretty good compared to manually written ASM, in the few cases where you have an extreme bottleneck that benefits highly from ultra optimization there are libraries for just those core performance primitives, and the rest of the program can stay portable and high level.
For those interested in HPC, have a look at
http://people.ds.cam.ac.uk/nmm1/ Of particular relevance to this thread are the sections on what you have to do to avoid "surprises" with C/C++, and also the tenuous relationships between computer arithmetic and maths. It is not beginner material. It is based on personal experience since the 1960s.
It is a bit surprising that there aren't more "formal methods" used to express algorithms and data structures and state machines and so on though so that more such "boilerplate" patterns and program elements can actually be "provably correct" and also more easily analyzable with respect to side effects, execution time, dependencies, hazards, error cases, etc. When you look at "design patterns" you see a lot of them implemented in high level languages but not so much integration of them into almost "atomic" memes / atoms of program construction so that you can sort of take the HLL out of the picture for those "elemental blocks / patterns" and then have a HLL that is more designed around working at the levels in between and above those pattern elements.
Yes and no.
"State space explosion" and the halting problem are "issues" for FSMs. In other cases the formal methods are more difficult than the code, and even if you do something useful there are two problems: ensuring correct mapping to a program, and interfacing with the non-formal stuff outside the proof.
As for design patterns, it is usually easier to throw something together, do a few unit tests to get a green light, ship the product and get customer service to deny there are intermittent problems
If you are interested in this topic, have a look at xC on the XMOS processors. It enables CSP/Occam style programming and interfacing with external devices on multicore processors, and the development environment will tell you exactly how fast each block will execute.
For example, there is hardware and
language support to allow output to occur on a specific (500MHz) clock cycles, and waiting for inputs to change and recording the new value and clock cycle at which it occurred.