Language Suggestions

"A proof is a program; the formula it proves is a type for the program."

This is beautiful.

I'm currently studying type theory and I would like to try new programming languages, maybe even experimental ones, which employ this kind of formalism and reasoning in its design.

However, it seems that, for some reason, most popular functional languages I've tried have an awkward and totally unreadable syntax, at least for me. In my opinion, ML and derivatives are doable, but right on the edge; Haskell, Epigram, Erlang, Agda, and others, feature pretty incomprehensible syntax. I would not imagine myself teaching any of these languages to a non-programmer, for example.

Are there any languages, with such a mathematical design, which has sane syntax (even if more verbose) and which can be used to create useful, practical programs?

What /prog/ comes up with?

Are there any languages, with such a mathematical design, which has sane syntax (even if more verbose) and which can be used to create useful, practical programs?
seriously, Scala is the only language that qualifys as fully functional with the option of only having to use functional programming when you need it. It is a huge mistake to think you can pick up a language like Haskell or ML or even Lisp without a full background in functional data structures. Unlike languages like Python, Javascript, Lua, etc that throw in a few functional features, Scala is the only language where you can transition to a fully functional paradigm