Unfortunately the "proofs" in dependently typed languages are extremely long and tedious to write. Some kind of compiler proofing tool could ease the pain, but I do not think it has low enough complexity for a GSoC project.
I wouldn't say that. Here's the complete proof script in Coq proving the theorem that was originally proposed: length (map f (xs ++ ys)) = length xs + length ys. It weighs in at about 30 lines, although I could probably get it down to less than 10. The proofs maybe look a bit unfamiliar if you haven't seen Coq before, but they are hardly "extremely long and tedious to write". I can understand that raw proof *terms* in type theory can be long and painful to write. But that's like saying Haskell is bad, because its hard to understand ghc-core. Wouter Require Import List. Variables a b : Set. Variable f : a -> b. Lemma lengthMap : forall (xs : list a), length (map f xs) = length xs. Proof. intros. induction xs; trivial. simpl; rewrite IHxs. reflexivity. Qed. Lemma appendLength : forall (xs ys : list a), length (xs ++ ys) = length xs + length ys. Proof. intros. induction xs; trivial. simpl; rewrite IHxs. reflexivity. Qed. Lemma main : forall (xs ys : list a), length (map f (xs ++ ys)) = length xs + length ys. Proof. intros. rewrite lengthMap. rewrite appendLength. reflexivity. Qed.