Congratulations! You just Blub Paradox'd yourself. At this point in your knowledge cycle, you are unable to understand something more complex than what you already know.
Knowledge is power. Defending your own knowledge by refusing to expand and learn something new is cutting yourself off at the knees (or fingers, as it may be).
The subtext of your challenge is that no language could possibly exist that is substantially better than PHP at expressing a solution to any problem, which would mean there's little to be gained by learning anything else. That's not a claim I'd ever make about my favorite languages, even though nobody makes huge lists of indefensible design gaffes in those.
I for one will freely admit that my Haskell still sucks and so I presume I'm not even smart enough yet to start on Agda. Do you recommend it? Do you find it to be (one of) the highest known point on the power continuum?
Oh, I'm still stuck at Haskell, which doesn't suck but could be better. A friend of mine did some playing around with automated proof assistants, and I've been to some talks about seL4, a microkernel prototyped in Haskell, written in C, and proven correct in Isabelle.
From Haskell you can of course go the route to Agda or Isabelle. But Curry is also worth a visit, it combines logical and functional languages.
I, for one, am still learning how to do left-fold based IO in Haskell with enumerators, at the moment.
Knowledge is power. Defending your own knowledge by refusing to expand and learn something new is cutting yourself off at the knees (or fingers, as it may be).