3 ms·

Then you've left the realm of formal specification of systems, though, so you're entirely outside the scope of the problem.

by hwayne 6y ago

scotty79 6y ago
No. I haven't left anything. I'm just saying that expecting that useful widespread formal specification language will be something as simple as LTT is wildly optimistic and you should expect that it will rather mirror and encompass the complexities and requirements of actual programming, like necessity of composability. And it will most likely be somewhere between practical but unsound specification languages and those that come from pure mathematics.
- hwayne 6y ago
  I used LTL because it's simple enough to explain the core ideas without getting bogged down in affordances and details. It's purely a pedagogical choice, just like how nobody explains the halting problem in terms of Java. Switching to a different notation helps with some of the practical details, but doesn't remove the essential problems that arise in composing specs.
  - scotty79 6y ago
    The sorce of the problem with composability in this post is that you don't have a concept of sub-states and 'partial next' operators.
    - hwayne 6y ago
      Would you be willing to provide a full example, replicating the dependent spec?
      - Pet_Ant 6y ago
        I'm wondering if you could as part of the O operator list all the variables in consideration for the "next"-state asar as that operator is concerned. like O[a,b,c]X in the next state which is determined by a change to any of a, b, or c, then X will be true. In the case where the set of variables is all of them they can be omitted and thus get the existing behaviour. I also suspect that the O operator with with a subset of variables will behave identically to other instances with the same set. However, I feel like this will still hit walls before practical limits, Beth would just need a non-trivial example
- Pet_Ant 6y ago
  It must be sound or it's of no use. Reminds me of the Ultraviolet Catastrophe. They had a theory that gave them precise answers, they just happened to be blatantly wrong.
  - scotty79 6y ago
    Unsound things can be useful. https://frenchy64.github.io/2018/04/09/unsoundness-reply.html https://frenchy64.github.io/2018/04/09/unsoundness-reply.htm...

Then you've left the realm of formal specification of systems, though, so you're entirely outside the scope of the problem.

by hwayne 6y ago

Then you've left the realm of formal specification of systems, though, so you're entirely outside the scope of the problem.

scotty79 6y ago

No. I haven't left anything. I'm just saying that expecting that useful widespread formal specification language will be something as simple as LTT is wildly optimistic and you should expect that it will rather mirror and encompass the complexities and requirements of actual programming, like necessity of composability. And it will most likely be somewhere between practical but unsound specification languages and those that come from pure mathematics.

hwayne 6y ago
I used LTL because it's simple enough to explain the core ideas without getting bogged down in affordances and details. It's purely a pedagogical choice, just like how nobody explains the halting problem in terms of Java. Switching to a different notation helps with some of the practical details, but doesn't remove the essential problems that arise in composing specs.
- scotty79 6y ago
  The sorce of the problem with composability in this post is that you don't have a concept of sub-states and 'partial next' operators.
  - hwayne 6y ago
    Would you be willing to provide a full example, replicating the dependent spec?
    - Pet_Ant 6y ago
      I'm wondering if you could as part of the O operator list all the variables in consideration for the "next"-state asar as that operator is concerned. like O[a,b,c]X in the next state which is determined by a change to any of a, b, or c, then X will be true. In the case where the set of variables is all of them they can be omitted and thus get the existing behaviour. I also suspect that the O operator with with a subset of variables will behave identically to other instances with the same set. However, I feel like this will still hit walls before practical limits, Beth would just need a non-trivial example
Pet_Ant 6y ago
It must be sound or it's of no use. Reminds me of the Ultraviolet Catastrophe. They had a theory that gave them precise answers, they just happened to be blatantly wrong.
- scotty79 6y ago
  Unsound things can be useful. https://frenchy64.github.io/2018/04/09/unsoundness-reply.html https://frenchy64.github.io/2018/04/09/unsoundness-reply.htm...