Well, apparently someone rewrote it in rust, which was better than their version. Which they needed some time to process how to continue.

And they got stuck with the bounds checker and loops.

But other such checkers are far more advanced, with a better contract syntax.