2 added 735 characters in body

Gildenhuys, Ribes and Zakesskii and others have developed a Bass-Serre theory for profinite groups acting on profinite trees. Using this theory, Ribes and Zalesskii showed that if $H_1,\ldots,H_n$ are finitely generated subgroups of a free group then the subset $H_1\cdots H_n$ is closed in the profinite topology. This was a conjecture by people working in semigroup theory and automata theory that is essentially equivalent to a conjecture of Rhodes in semigroup theory. The Ribes and Zalesskii proof does not use approximation by finite groups, but rather the geometry of these profinite trees. Other proofs using geometric group theory and using model theory now exist.

Recently Almeida assigned profinite groups to irreducible symbolic systems in a way that is functorial up to inner automorphism. Again finite groups do not explicitly appear in the discussion.

UPDATE: Another aspect of the theory of profinite groups as objects in their own right is the study of just infinite profinite groups. An infinite profinite group is just infinite if all its non-trivial closed normal subgroups are open. For example, the p-adic integers are just infinite. Just infinite is the analogue of simple for infinite profinite groups. Every finitely generated infinite profinite group has a just infinite quotient. There is a trichotomy due to Wilson (and refined by Grigorchuk) describing what they can look like. The study of just infinite profinite groups is connected to the theory of profinite branch groups and actions on rooted trees. See the handbook chapter by Bartholdi, Grigorchuk and Sunik.

Gildenhuys, Ribes and Zakesskii and others have developed a Bass-Serre theory for profinite groups acting on profinite trees. Using this theory, Ribes and Zalesskii showed that if $H_1,\ldots,H_n$ are finitely generated subgroups of a free group then the subset $H_1\cdots H_n$ is closed in the profinite topology. This was a conjecture by people working in semigroup theory and automata theory that is essentially equivalent to a conjecture of Rhodes in semigroup theory. The Ribes and Zalesskii proof does not use approximation by finite groups, but rather the geometry of these profinite trees. Other proofs using geometric group theory and using model theory now exist.