Epigram has got a type system which is strong enough to express the behaviour of programs, the type checker then guarantees that the program is well behaved. However, you don't have to go as far, you can write ordinary programs and refactor them into more trustworthy, formally checked deliverables -- Epigram supports a pay as you go approach to formal methods.
Details of the current state of the project are available in the form of a developers' blog. Epigram source code is at a darcs pull away:
darcs pull http://www.e-pig.org/darcs/Pig09
In this space, following Darwin's tradition, we collect bugs. Sometimes, we might fix them. More often than not, someone not running after a PhD thesis will. Don't laugh, that could be you.