Yes, Idris. Dependent types in an effect system allow you to prove that deadlock cannot occur, such that a potential deadlock in user code is a compile time error. Edwin Brady has been working on this for decades[1], and Idris 2[2] has finally made it a reality[3].

1. https://www.type-driven.org.uk/edwinb/papers/fi-cbc.pdf (free; 2009)

2. https://livebook.manning.com/book/type-driven-development-wi... (registration wall; 2017)

3. https://research-repository.st-andrews.ac.uk/handle/10023/23... (free; 2021)