out of curiosity, is haskell already been used as a "specification" language ? i was thinking in a business term, rather than mathematical one. (i.e. one than " normal mortal can read, even with a bit of training ;-) I.e. one would specifiy a model, an application ( possibly run it on samples), and hand it over to developper, typically in other languages/environment... I am aware of the contracts paper of SPJ, for instance... others you may think of ? does a spec. always leads to a DSL , for instance ? I imagine a specification for an application resulting in a DSL for the "data model"/ " process model " part, (which is the generic/ reusabel part, IMH) plus something more specific to the effective application targeted... (I cannot resist explaining my long term view : if IT outsourcing really takes off one day, one key factor will be proper specification, which is in a dear state in the current practice nowadays "in the field") ref: http://search.ft.com/search/article.html?id=030923007625