It's possible; we can only make a comparison based on those aspects of the design that have been publicly disclosed, so we can only really address the question of MSOL vs. MLTT. Both HMC and Ohad claim to know the answers here, but their answers are in contradiction with each other. Previously I had thought I was able to demonstrate the insufficiency of MSOL but upon closer analysis I realized that my proofs were based on flawed assumptions and misinterpretations. Since coming to this realization, have taken a step back from "pushing the MLTT agenda", and now my goal is simply to play the role of a neutral 3rd party and analyze the validity of these claims, along with carrying out some further research into the strengths and weaknesses of various other logical systems that could potentially be used (mainly just standard systems discussed frequently in academic literature on formal logic, as these have the most metatheoretic results available to aid in the comparisons, and are the most likely systems to be brought up as an actual candidate logic as MSOL and MLTT have). I'll share my results with the community as I go along, on the AutoNomic wiki, though I will warn ahead of time that the explanations will still be very technically involved; it's simply a complex subject.