5 ms·

To me "formal specification" sounds like it should have some sort of connection to formal methods, i.e., some proof system. This looks more like what I would ca

To me "formal specification" sounds like it should have some sort of connection to formal methods, i.e., some proof system. This looks more like what I would call an "instruction set simulator". Though if the focus is on clarity and readability rather than performance, "executable specification" might be a good middle ground.

contravariant 7y ago
In this context "formal" just means that no parts are left open to interpretation [1]. While proof systems are definitely formal that implication doesn't work the other way around. Under normal circumstances programming code is unambiguous and should therefore suffice as a formal definition / specification (with most programming errors stemming from the fact that this formal definition doesn't match the informal definition the programmer or customer had in mind). [1]: For comparison, https://en.wiktionary.org/wiki/formal https://en.wiktionary.org/wiki/formal defines 'formal' as: "(mathematics) Relating to mere manipulation and construction of strings of symbols, without regard to their meaning".
- deleted 7y ago
  [deleted]
- tom_mellior 7y ago
  > 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
monocasa 7y ago
It's the first step in a lot of formal methods. Like proving an implementation's adherence to the model requires a machine readable model. Or proving certain aspects about the model. For instance part of sel4's proof chain is a machine readable model of an ARM. It then uses that to prove equivalence of the generated binary to the high level spec of the kernel.

contravariant 7y ago

In this context "formal" just means that no parts are left open to interpretation [1]. While proof systems are definitely formal that implication doesn't work the other way around. Under normal circumstances programming code is unambiguous and should therefore suffice as a formal definition / specification (with most programming errors stemming from the fact that this formal definition doesn't match the informal definition the programmer or customer had in mind). [1]: For comparison, https://en.wiktionary.org/wiki/formal https://en.wiktionary.org/wiki/formal defines 'formal' as: "(mathematics) Relating to mere manipulation and construction of strings of symbols, without regard to their meaning".

deleted 7y ago
[deleted]
tom_mellior 7y ago
> 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

monocasa 7y ago

It's the first step in a lot of formal methods. Like proving an implementation's adherence to the model requires a machine readable model. Or proving certain aspects about the model. For instance part of sel4's proof chain is a machine readable model of an ARM. It then uses that to prove equivalence of the generated binary to the high level spec of the kernel.