3 ms·

There are formal methods both for specs (e.g. TLA+ checked by TLC and TLAPS) and for implementations (e.g. ADA-Spark checked by GNAT). The spec can indeed be ch

There are formal methods both for specs (e.g. TLA+ checked by TLC and TLAPS) and for implementations (e.g. ADA-Spark checked by GNAT). The spec can indeed be checked that invariants or liveness properties are honored. Some formal modeling tools for specs can actually extract implementations that satisfy the spec, though I think you're being nit-picky on the semantics of "create." Specs don't have to be English, you know. I write my specs for machines first and humans second.

ncmncm 7y ago
May I take "I write my specs for machines" to mean that you simply omit the parts of the specification that are not expressible in the formalism at hand? A specification with parts deliberately omitted is deliberately incomplete. An implementation of a sufficiently incomplete specification may be formally verified to satisfy the spec without ensuring much of anything, although it may suffice to justify payment. This attitude is typical in formal specification.
- sterlind 7y ago
  No, I didn't mean that. in my particular domain (a distributed systems library) I have a collection of specifications for things like commands, locks and collections, which are compact enough that I feel I can describe them fully. There has been one case where I had to simplify the model, which I consider a great failure, since that was the one time I had bugs appear that I didn't catch during model testing. Take the example of a reader/writer lock. I claim it's possible to completely define the spec of such a lock, so that any question about the intended behavior of the lock can be decided by the machine. Sure, it's a simple example, but my library is a collection of simple recipes. Do you disagree?
  - ncmncm 7y ago
    I agree that you can usefully, formally specify certain behaviors by choosing to ignore, e.g., implementation details. There are a lot of implementation details: stack depth, instruction mix, power consumption, timing fluctuation, memory placement. Incorporate too many, and you lose clarity, even usability. But implementation details are often what hackers rely on. So, yes, formal modeling is useful, sometimes essential, but does not eliminate hackability. Overselling it does harm.

ncmncm 7y ago

May I take "I write my specs for machines" to mean that you simply omit the parts of the specification that are not expressible in the formalism at hand? A specification with parts deliberately omitted is deliberately incomplete. An implementation of a sufficiently incomplete specification may be formally verified to satisfy the spec without ensuring much of anything, although it may suffice to justify payment. This attitude is typical in formal specification.

sterlind 7y ago
No, I didn't mean that. in my particular domain (a distributed systems library) I have a collection of specifications for things like commands, locks and collections, which are compact enough that I feel I can describe them fully. There has been one case where I had to simplify the model, which I consider a great failure, since that was the one time I had bugs appear that I didn't catch during model testing. Take the example of a reader/writer lock. I claim it's possible to completely define the spec of such a lock, so that any question about the intended behavior of the lock can be decided by the machine. Sure, it's a simple example, but my library is a collection of simple recipes. Do you disagree?
- ncmncm 7y ago
  I agree that you can usefully, formally specify certain behaviors by choosing to ignore, e.g., implementation details. There are a lot of implementation details: stack depth, instruction mix, power consumption, timing fluctuation, memory placement. Incorporate too many, and you lose clarity, even usability. But implementation details are often what hackers rely on. So, yes, formal modeling is useful, sometimes essential, but does not eliminate hackability. Overselling it does harm.