4 ms·

Yes, thanks for mentioning. It has been on my radar as well, but as I have seen its less universal and more focused on the verification of concurrent processes

by pezo1919 7y ago

Yes, thanks for mentioning. It has been on my radar as well, but as I have seen its less universal and more focused on the verification of concurrent processes - which is not the whole picture. But I will give a shot if there is nothing else.

pron 7y ago
TLA+ is just as good for non-concurrent stuff. It's just that it's one of the only things capable to naturally tackle arbitrary concurrency, so it gets more focus there.
- pezo1919 7y ago
  Good to know ty! What are the main differences (pros/cons) using TLA+ vs Dependent Types (and proving the algorithm is fine) for system verification?
  - pron 7y ago
    There are many subtle and less subtle differences, but the main difference is that TLA+ is being used in the industry to help design complex systems in various domains and of various scale, both hardware and software, while dependent types are still in research, and I am not aware of any project not done by a research institution or with the assistance of one to specify and verify a real world system using dependent types in any form resembling ordinary software development and with similar budgets. I am also not aware of any software deeply specified and verified with dependent types that exceeds a few thousand lines of code.
    - pezo1919 7y ago
      Ah okay, thanks! The complexity of Asynchronicity & Concurrency lead me to the formal expression of time related logic: Temporal Logic (https://en.wikipedia.org/wiki/Temporal_logic https://en.wikipedia.org/wiki/Temporal_logic) There are multiple temporal logics with different level of usefulness. (Check Temporal logics section.) I really want to solve harder problems and express deeper relations, so it seems to me what I’d need is CTL at least (https://en.wikipedia.org/wiki/Computation_tree_logic https://en.wikipedia.org/wiki/Computation_tree_logic). I thought I might want to model my software (any kind of app!) and prove it is working as intended using CTL (or other more expressive TL) in Agda/Idris (Coq/TLA+) and then make a similar implementation in another language. Eg. there is an LTL implementation in Agda, but I did not find similar things for CTL.(https://github.com/xekoukou/LTL https://github.com/xekoukou/LTL) What do you think, is it a good idea to express my model using (C)TL in Agda/Idris, or I should use a more dedicated piece of technology for that problem? Is there a limit in case of Agda/Idris for that in theory? Any resource is appreciated!
      - pron 7y ago
        TLA is also a (linear) temporal logic that's simpler than LTL, and it's at the core of TLA+. If you don't want to spend months studying and then months writing proofs as a learning experience but rather would like to actually specify and verify real systems, use a language with a temporal logic model checker, like TLA+ (that has the TLC model checker) or Promella (Spin). If you want the other kind of experience, there have been implementations of TLA in both Coq and Isabelle.

pron 7y ago

TLA+ is just as good for non-concurrent stuff. It's just that it's one of the only things capable to naturally tackle arbitrary concurrency, so it gets more focus there.

pezo1919 7y ago
Good to know ty! What are the main differences (pros/cons) using TLA+ vs Dependent Types (and proving the algorithm is fine) for system verification?
- pron 7y ago
  There are many subtle and less subtle differences, but the main difference is that TLA+ is being used in the industry to help design complex systems in various domains and of various scale, both hardware and software, while dependent types are still in research, and I am not aware of any project not done by a research institution or with the assistance of one to specify and verify a real world system using dependent types in any form resembling ordinary software development and with similar budgets. I am also not aware of any software deeply specified and verified with dependent types that exceeds a few thousand lines of code.
  - pezo1919 7y ago
    Ah okay, thanks! The complexity of Asynchronicity & Concurrency lead me to the formal expression of time related logic: Temporal Logic (https://en.wikipedia.org/wiki/Temporal_logic https://en.wikipedia.org/wiki/Temporal_logic) There are multiple temporal logics with different level of usefulness. (Check Temporal logics section.) I really want to solve harder problems and express deeper relations, so it seems to me what I’d need is CTL at least (https://en.wikipedia.org/wiki/Computation_tree_logic https://en.wikipedia.org/wiki/Computation_tree_logic). I thought I might want to model my software (any kind of app!) and prove it is working as intended using CTL (or other more expressive TL) in Agda/Idris (Coq/TLA+) and then make a similar implementation in another language. Eg. there is an LTL implementation in Agda, but I did not find similar things for CTL.(https://github.com/xekoukou/LTL https://github.com/xekoukou/LTL) What do you think, is it a good idea to express my model using (C)TL in Agda/Idris, or I should use a more dedicated piece of technology for that problem? Is there a limit in case of Agda/Idris for that in theory? Any resource is appreciated!
    - pron 7y ago
      TLA is also a (linear) temporal logic that's simpler than LTL, and it's at the core of TLA+. If you don't want to spend months studying and then months writing proofs as a learning experience but rather would like to actually specify and verify real systems, use a language with a temporal logic model checker, like TLA+ (that has the TLC model checker) or Promella (Spin). If you want the other kind of experience, there have been implementations of TLA in both Coq and Isabelle.