3 ms·

> In this context "formal" just means that no parts are left open to interpretation Yes. But as you say, by that token any instruction set simulator could be c

> In this context "formal" just means that no parts are left open to interpretation Yes. But as you say, by that token any instruction set simulator could be called a "formal specification" (modulo undefined behavior, or if you deliberately wrote in a language with nondeterminism). But we don't call them that, because (I maintain) there is something more to being a "formal specification". Namely, being in a form that is easily amenable to formal methods tools, and the intention to apply these tools. Now of course a pure F# or Haskell program is much closer than C to being analyzed by formal methods tools, but there is still a gap that wouldn't be there if the specification were written directly in Coq or Agda or Isabelle or whatever.

contravariant 7y ago
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