[tails4e]

This is interesting, it seems like it may in fact be testing by looping, given it took a minute, and didn't conclude. For hardware design there are logic equivalence checking tools that work very differently - they essentially work by reducing a function (piece of hardware) to a minimized boolean equation. The method of reduction ensures the same logic, no matter how coded, results in the same boolean equation, and then comparing the equations is direct and does not require testing all input values. Hardware verification also has a higher bar than software, where code coverage analysis can require 100% on line, branch, value, condition, expression, functional, etc. Its a lot of work, but does give very high confidence there are zero bugs.

[Choc13]

Hey, the reason for the long times on the playground is actually that we’re having to wait for build servers to boot up and then build the code before we can finally ship it off to our backend for analysis. We’ve had quite a bit of feedback on this slowness and we hope to eliminate some of this constant factor boot up and compile time soon, and for what remains make it clear that this is what’s happening in the status box.

So although it might seem like it, we’re not actually doing any looping, we’re doing constraint solving as you’ve mentioned.