Are we not confusing difficulty with familiarity? For me personally, as someone very familiar with FP, Idris was very approachable and easy to at least write simple proofs in.