The development of
ra.hs has called for an interesting task in the domain of symbolic programming.
ra.hs is a Haskell linter for reactive programs, the first implementation I'm undertaking to identify possible race conditions in reactive code. The violation to look for is a subtle one: if two threads consume the same stream and read and write these values to the same shared memory, the ordering rules of the stream might be violated [citation to come]. To decide this, it's necessary to trace the flow of values through the program to see which stream they come from, if any.
The degree of sophistication of analysis against the program could be incredibly varied, bounded above only by the undecideability of the halting problem (fun fact: with probability 1, halting can actually be decided). I believe that it's meaningfully bounded below by a type analysis, where the conditional nature of branches is ignored and all values that are the correct type that could flow to a call site are considered. This allows for a perfectly sensitive result that sacrifices specificity (i.e. it may report many false positives).