4 ms·

What I find most remarkable about the comments here is how quickly programmers try to jump to code (I'm not passing judgment, just making an observation). The g

by pron 8y ago

What I find most remarkable about the comments here is how quickly programmers try to jump to code (I'm not passing judgment, just making an observation). The goal of this post is to present a simple yet useful specification tool. Sure, a decision table implemented in Clojure would likely be more readable than one implemented in assembly, but figuring out what the decisions should be would be far, far more costly and significant (in all interesting cases) than implementing, or reading, either. Sometimes a specification is not even implemented in a single program, but in some distributed system, with no direct representation in code, and sometimes a specification specifies the environment the system interacts with, and is not even implemented by a computer at all. Coding is important, but specifying is usually much more so, as it is both more costly and has a higher impact. Developers should learn how to think about specification and use various aids -- like decision tables -- without thinking at the code level, which is often a distraction.

jmmcd 8y ago
I agree, but what's even better than a specification is an executable specification. If we see a decision table as data (see discussion below) then it can be both -- no chance for the implementation to go out of sync with the spec, and "don't repeat yourself".
- pron 8y ago
  Good specifications are often written at a level that generating executable code from them is often undecidable and almost always intractable in practice. What would really be nice -- although we have not been able to achieve even that at scale yet -- is a formal refinement between implementation and specification (i.e. you can't execute the specification, but you can ensure it's in sync). There are, however, various techniques that can do so approximately [1]. But I believe that even a good spec without any formal tie to code (which we certainly can do) gives you 90% of the value of a spec that is formally tied to the code (which we don't know how to do just yet). [1]: E.g. trace-checking: https://arxiv.org/pdf/1111.2825.pdf https://arxiv.org/pdf/1111.2825.pdf
  - espeed 8y ago
    > Good specifications are often written at a level that generating executable code from them is often undecidable and almost always intractable in practice. What about modern dependently-typed meta languages like Idris and program synthesizers like Nadia Polikarpova's work on Synquid? Type-Driven Program Synthesis, by Nadia Polikarpova (StrangeLoop 2018) [video] https://www.youtube.com/watch?v=HnOix9TFy1A https://www.youtube.com/watch?v=HnOix9TFy1A MIT Comcom: Synquid program synthesizer, and more command-line tools for the web http://comcom.csail.mit.edu/comcom/ http://comcom.csail.mit.edu/comcom/ Idris Software Foundations https://github.com/idris-hackers/software-foundations https://github.com/idris-hackers/software-foundations
    - pron 8y ago
      We don't know how to scale those [1]. It's very easy to specify a simple sorting function in Idris/Java with JML and prove it correct. It's a whole other matter to specify the global properties of an entire system, and verify them all the way down to the small bits of code. Various code synthesis tools are even more limited, as they tend to rely heavily on fragile automated reasoning tools like SMT solvers, although both are orders of magnitude away from being able to handle real applications that I think that comparing them to one another is a bit beside the point. The biggest programs ever written and verified with deductive proofs -- be it dependently typed languages or any verification based on deduction, correspond at most to ~10,000 LOC of C, taken years of work by academic experts, and had to be significantly simplified to make proofs easier (i.e., they had to use only the simplest data structures, etc.). In contrast, business applications are 2-3 orders of magnitude bigger. [1]: And when I say "we don't know" I mean that it is possible that some time in the next 2-5 decades we may be able to do something, but it's also possible that there are fundamental complexity limitations that mean that this particular path will never lead to something similar to what we may imagine it could.
  - emmanueloga_ 8y ago
    I've been thinking a bit about model driven development. I think what you say is true, but at a bare minimum the specification should be machine readable. Take the IRC RFC, for instance. A lot of it is amenable to code generation, but machine-parsing the spec is so hard (I know.. I tried, many moons ago). I feel like a big chunk of that spec could be written in such way that a big part of an IRC client or server could be generated. For other parts, a generator could at least create boilerplate to be filled by a human and maybe some automatic tests.
- jonathanstrange 8y ago
  I once had an argument about that. A very smart colleague of mine claimed to have specified a very complete natural language tense system in Mercury, sort of hard-coded into the language if I understood him correctly. He claimed that it was way better than what general semanticists had come up with and that the use of logic in semantics is totally superfluous. My point was that it doesn't matter how good his system is, as long as he doesn't separate declaration from implementation, it will be of almost no use. Nobody will be able to run his Mercury program in 100 years from now. Then again, it's not possible to run my Higher Order Logic with Henkin models and Categorial Grammar out of the box either. So I'm still not sure who had the better argument. Maybe if researchers could agree on a common programming language, we could indeed dispense with descriptive formalisms?
deleted 8y ago
[deleted]
pathseeker 8y ago
>Coding is important, but specifying is usually much more so Lacking code, however, usually leads to important oversights in the specifications. Internet routers had to have a "compatible with Cisco" option because Cisco engineers read a specification, wrote an implementation, had no reference code to test against, and ended up with a widely deployed broken protocol incompatible with the correct version. Code is critical for specifications because it doesn't suffer the flaws of human interpretation and assumptions. If it does disagree with human interpretations of the specification then it quickly becomes obvious and either the code or specification can be fixed in a revision.
- pron 8y ago
  > Code is critical for specifications because it doesn't suffer the flaws of human interpretation and assumptions. Code is a formal specification at a very particular level. But you can have formal specifications of any level you like that is just as precise and mechanical as code (and usually much clearer).

by pron 8y ago

jmmcd 8y ago

I agree, but what's even better than a specification is an executable specification. If we see a decision table as data (see discussion below) then it can be both -- no chance for the implementation to go out of sync with the spec, and "don't repeat yourself".

pron 8y ago
Good specifications are often written at a level that generating executable code from them is often undecidable and almost always intractable in practice. What would really be nice -- although we have not been able to achieve even that at scale yet -- is a formal refinement between implementation and specification (i.e. you can't execute the specification, but you can ensure it's in sync). There are, however, various techniques that can do so approximately [1]. But I believe that even a good spec without any formal tie to code (which we certainly can do) gives you 90% of the value of a spec that is formally tied to the code (which we don't know how to do just yet). [1]: E.g. trace-checking: https://arxiv.org/pdf/1111.2825.pdf https://arxiv.org/pdf/1111.2825.pdf
- espeed 8y ago
  > Good specifications are often written at a level that generating executable code from them is often undecidable and almost always intractable in practice. What about modern dependently-typed meta languages like Idris and program synthesizers like Nadia Polikarpova's work on Synquid? Type-Driven Program Synthesis, by Nadia Polikarpova (StrangeLoop 2018) [video] https://www.youtube.com/watch?v=HnOix9TFy1A https://www.youtube.com/watch?v=HnOix9TFy1A MIT Comcom: Synquid program synthesizer, and more command-line tools for the web http://comcom.csail.mit.edu/comcom/ http://comcom.csail.mit.edu/comcom/ Idris Software Foundations https://github.com/idris-hackers/software-foundations https://github.com/idris-hackers/software-foundations
  - pron 8y ago
    We don't know how to scale those [1]. It's very easy to specify a simple sorting function in Idris/Java with JML and prove it correct. It's a whole other matter to specify the global properties of an entire system, and verify them all the way down to the small bits of code. Various code synthesis tools are even more limited, as they tend to rely heavily on fragile automated reasoning tools like SMT solvers, although both are orders of magnitude away from being able to handle real applications that I think that comparing them to one another is a bit beside the point. The biggest programs ever written and verified with deductive proofs -- be it dependently typed languages or any verification based on deduction, correspond at most to ~10,000 LOC of C, taken years of work by academic experts, and had to be significantly simplified to make proofs easier (i.e., they had to use only the simplest data structures, etc.). In contrast, business applications are 2-3 orders of magnitude bigger. [1]: And when I say "we don't know" I mean that it is possible that some time in the next 2-5 decades we may be able to do something, but it's also possible that there are fundamental complexity limitations that mean that this particular path will never lead to something similar to what we may imagine it could.
- emmanueloga_ 8y ago
  I've been thinking a bit about model driven development. I think what you say is true, but at a bare minimum the specification should be machine readable. Take the IRC RFC, for instance. A lot of it is amenable to code generation, but machine-parsing the spec is so hard (I know.. I tried, many moons ago). I feel like a big chunk of that spec could be written in such way that a big part of an IRC client or server could be generated. For other parts, a generator could at least create boilerplate to be filled by a human and maybe some automatic tests.
jonathanstrange 8y ago
I once had an argument about that. A very smart colleague of mine claimed to have specified a very complete natural language tense system in Mercury, sort of hard-coded into the language if I understood him correctly. He claimed that it was way better than what general semanticists had come up with and that the use of logic in semantics is totally superfluous. My point was that it doesn't matter how good his system is, as long as he doesn't separate declaration from implementation, it will be of almost no use. Nobody will be able to run his Mercury program in 100 years from now. Then again, it's not possible to run my Higher Order Logic with Henkin models and Categorial Grammar out of the box either. So I'm still not sure who had the better argument. Maybe if researchers could agree on a common programming language, we could indeed dispense with descriptive formalisms?

deleted 8y ago

[deleted]

pathseeker 8y ago

>Coding is important, but specifying is usually much more so Lacking code, however, usually leads to important oversights in the specifications. Internet routers had to have a "compatible with Cisco" option because Cisco engineers read a specification, wrote an implementation, had no reference code to test against, and ended up with a widely deployed broken protocol incompatible with the correct version. Code is critical for specifications because it doesn't suffer the flaws of human interpretation and assumptions. If it does disagree with human interpretations of the specification then it quickly becomes obvious and either the code or specification can be fixed in a revision.

pron 8y ago
> Code is critical for specifications because it doesn't suffer the flaws of human interpretation and assumptions. Code is a formal specification at a very particular level. But you can have formal specifications of any level you like that is just as precise and mechanical as code (and usually much clearer).