6 ms·
tla+ solves a similar problem but isn't exactly what you're describing
by xhgdvjky 7y ago
tla+ solves a similar problem but isn't exactly what you're describing
- pezo1919 7y agoYes, 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 agoTLA+ 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 agoGood 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 agoThere 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 agoAh 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 agoTLA 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.
- RBerenguel 7y agoAlloy as well, if you are just trying to reduce search spaces.
- pezo1919 7y agoDid not know about it, ty.
- pezo1919 7y agoThanks!