The main reason code isn't considered a formal specification is that it's not intended to be either formal or a specification. That doesn't mean you cannot writ

The main reason code isn't considered a formal specification is that it's not intended to be either formal or a specification. That doesn't mean you cannot write a formal specification in code. If anything code allows for a higher level of formality than all but the most formal mathematics. Which is why some mathematicians are advocating that mathematical proofs should be specified as code [1]. You shouldn't confuse the existence of these languages to mean that any code not capable of expressing mathematical proofs is not formal. It might be limited, but not informal. [1]: https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE