Hi

To see at a glance the various bug reports about fromJust you can search the bug database: http://bugs.darcs.net/issue?@columns=id%2Cactivity%2Ctitle%2Ccreator%2Cassignedto%2Cstatus&@sort=activity&@group=priority&@search_text=fromJust

I count 7 bugs.

I would be interested to see the results of static analysis tools (Catch?) or applying Oleg's strategy. Any volunteers?

Unfortunately darcs is too big, and too unhaskell-98 to go through Catch as it currently stands. In reality the best strategy would probably be to use Catch on darcs, then where Catch is unable to automatically verify the program use Oleg's techniques and other rewritings until Catch can verify everything. Just taking a random example (the first fromJust I stumbled upon): http://abridgegame.org/repos/darcs-unstable/Population.lhs, cleanPop The requirement here is that the modifiedHowI field of the 2nd field of the Pop at the top must be not a removal. Figuring out in an existing code-base whether that is a general invariant for Pop, true in this specific case, or any other random combination is quite a hard problem! Thanks Neil