Shmi comments on Algorithmic formalization of FDT?