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?

>>4
I totally disagree. We've all had our share of C++ already.

>>9
I did. I enjoy Prolog a lot, but I can't see how to use Prolog for things other than experimentation and development of very specific kinds of programs. I can't see either how is it manageable (or even possible) to write, for example, a web server in Prolog.

I'm looking for languages of that sort that can be used to create useful, practical day-to-day programs and applications.

>>15
Interesting. I'll put Scala on my list of to-see languages.

In my opinion, it does not matter whether a language implements some or other paradigm -- a programming language must be usable, comprehensible and practical, otherwise it is of no use, at least not as a programming language.

>>22
Somewhat sadly, I use Gentoo.

>>24
OCaml is what I'm reading about these days. However, I don't like object-orientation; I think that OO (the way it is today) is the worst development model ever invented.