[thesz]

There is interesting video from RSC2010: http://video2010.scottishrubyconference.com/show_video/11/1

"Dependent Types: A Look At The Other Side" by Larry Diehl

It talks about using Types for Driving your Development. So it is TDD, but without tests, without runtime and programmer's overhead of them.

When using TyDD, you isolate core that should go as bugless as possible and write DSeL for it in language with strong type system. The talk above tells about Agda, but we and some number of other companies in the world (Eaton http//eaton.com/, Echo http://aboutecho.com/ - from the top of my head) successfully employ Haskell for that task.

That way you shoot two birds with one stone: you get provably correct software and you get an ideal language to express your core problems.

Best of all, you get free "requirement tracking" - whenever your requirements change, you express them in types and then apply changes where they should, guided by friendly compiler. Still getting provably correct software (modulo types) at the end.

[mdaniel]

That was "interesting" in that I like expanding my horizons, but it was a terrible presentation. Plus, it looks like Haskell and I got the impression from his lead-in that he was going to introduce a new language.

However, I actually came here to say something else about his material: if it is harder to decompose the business requirement into Haskell than it is to write monkey tests for one's Blub language, I am not certain anyone wins when going with a provably correct implementation.

[thesz]

He talked about Agda2.

My experience using advanced type system tells me that you can get away with functional tests. Types, also, takes much less code space-programmer's time than tests.

So I do not see how they could be harder to use. Certainly types will be unusual, but not much harder.