The only formal specification of a software is the software itself. If there would exist a way to specify exactly what a program should do formally you wouldn't

The only formal specification of a software is the software itself. If there would exist a way to specify exactly what a program should do formally you wouldn't need the programmer: you already have the formal specification, can't you just compile that to executable code? A formal specification doesn't make a lot of sense, if no sense at all. It's a waste of time and you will end up doing the work two times, one to write the specification and then to translate that specification in a real programming language. The most difficult part of the job of the programmer is not into writing the code, it's into translating the informal specification from the customer to a formal specification in the form of computer code.