8 Aug
2009
8 Aug
'09
6:30 a.m.
2009/8/7 Zachary Turner
Out of curiosity, is it impossible due to technical limitations, or is it just not implemented because it's either difficult or nobody's ever gotten around to it?
Undecidable by reduction to the halting problem in general, though apparently possible for straight-line code (no loops/recursion) through the brute-force method of generate all paths and send them to a theorem prover to prove equivalence.