Melyik a kedvenc programozási nyelved?

Bocsánat, kimaradt egy fontosabb példa:

vect_concat : ∀ (T : Type) (m n : ℕ) → Vector T m → Vector T n → Vector T (m + n)

vect_concat = ...

Itt látszik szépen, hogy a típusrendszer fordítási időben végez el olyasmit, ami felületesen futási idejű assertnek tűnne.

Ennek megvan persze az ára, ami miatt egyfajta plusz hozzáadott munkát is igényel a programozás, de egészében véve mégis ad egy koncepcionális segítséget a nyelv elmélyítése, és - ezt már nem tudom felmérni, mert még nem ismerem eléggé - de úgytudom eléggé messze is vezet ez az út:

[link]

[link]