Logic and type systems have been connected since Frege (he coined "functional" and "non-functional" types[1]). Computation friendly is interesting, but not real

Logic and type systems have been connected since Frege (he coined "functional" and "non-functional" types[1]). Computation friendly is interesting, but not really revolutionary. Topology I'm not an expert in so I can't comment. [1] On Function and Concept, 1891; http://fitelson.org/proseminar/frege_fac.pdf http://fitelson.org/proseminar/frege_fac.pdf