zypeh
says to
YSITD
然后丢掉所有电脑概念，学 Z3 和 Type system