[Dependent Types][Temporal Logic][Model Checkers] The complexity of Asynchronicity & Concurrency lead me to the formal expression of time related logic: 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). 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) 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! @Sankha Narayan Guria @Kartik Agaram

This is interesting. I don't have much experience with Agda/Idris. I have heard they are great tools - but the proof burden is high and modelling a real software is often challenging. It would definitely doable though. It would be great if you can share your experiences.