A simpler proof of Fermat's Last Theorem?

Via my former student Stijn de Vos, I just heard that Colin McLarty, a professor of philosophy and logician at Case Western Reserve University (who I remember briefly meeting at a conference in Uppsala a few years ago), claims that it should be possible to formulated a much simpler proof of Fermat's Last Theorem, when compared to Wiles' 110-page monster. As is well known, Wiles' proof relies heavily on the theoretical machinery introduced by Grothendieck. Quoting from a Science Daily article:

McLarty calls Grothendieck's work "a toolkit," and showed, at the Joint Mathematics Meetings in San Diego in January, that only a small portion is needed to prove Fermat's Last Theorem. [...]   "Where Grothendieck used strong set theory I've shown he could do with only a fraction of it," McLarty said. "I use finite-order arithmetic, where all sets are built from numbers in just a few steps. You don't need sets of sets of numbers, which Grothendieck used in his toolkit and Andrew Wiles used to prove the theorem in the 90s."

According to the article, Ohio State emeritus Harvey Friedman has described McLarty's result as a "clarifying first step". McLarty retorts:

"Fermat's Last Theorem is just about numbers, so it seems like we ought to be able to prove it by just talking about numbers," McLarty said. "I believe that can be done, but it will require many new insights into numbers. It will be very hard. Harvey sees my work as a preliminary step to that, and I agree it is."

This sounds like a very exciting development, and I for one look forward to seeing where it will go. Any M-Phi'ers around with insider's knowledge on the whole thing? I could not find further info over at McLarty's website.

UPDATE: Here is a relevant article by McLarty, 'What does it take to prove Fermat's Last Theorem?', published in the Bulletin of Symbolic Logic in 2010 (haven't read it yet).