If you had a multi-billion dollar software company, where would you spend your research money?
Why, solving the termination problem, of course! (Actually, if you read the fine print, the project isn't attempting to actually solve the termination problem, just solve it most of the time.)
Oh, and they're hiring. Brainiacs only, please. ;-)
As long as they have a heuristic to determine when decidability itself is undecideable (e.g., we've spent 20ms on this one, I guess it's toast), things which are not doable in general can be doable in practicallity. If your code is so obscure that the Terminator gives up on it, that could be a good reason to fail a code review -- unless it's a requirement. Of course, a proof of termination
F# is ML.net not Fortran.Net? There's a naming problem here! Interesting that they're using two variants of ML plus Prolog, and plain ol' C++. I miss Prolog, I'm looking forward to Perl6 Rules for that reason.
