These properties of a finite algebra A, referring to the variety V(A) generated by A, are undecidable: V(A) is residually finite, is residually small, is finitely axiomatizable, has a model companion, has type-set excluding the Boolean type (defined in tame congruence theory). All these results were proved in the past three years by the same method, which successfully models the computations of a Turing machine on an infinite tape by using elements of a power algebra A^\omega to represent instantaneous configurations in the computation, and using algebraic operations to model the transition between configurations produced by the Turing machine.

It is likely that this method can be used to obtain further interesting undecidability results. In the talk, I shall discuss some possible results of this kind, and examine in some detail the application which is closest to the origin of the method, namely the undecidability of the residual smallness of V(A).