Am Donnerstag, 19. Februar 2009 11:35 schrieb Alberto G. Corona:
2009/2/19 Wolfgang Jeltsch
Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain:
Haskell is a nice, mature and efficient programming language. By its very nature it could also become a nice executable formal specification language, provided there is tool support.
Wouldn't it be better to achieve the goals you describe with a dependently typed programming language?
But I wonder how a dependent typed language can express certain properties, for example, the distributive property between the operation + and * in a ring or simply the fact that show(read x)==x. As far as I understand, a dependent type system can restrict the set of values for wich a function apply, but it can not express complex relationships between operations.
Each type system corresponds to some constructive logic and can enforce properties which are expressible in that logic. Dependent type systems correspond to higher order predicate logics or so and therefore can express almost everything you want. An Agda or Epigram type can cover a complete behavioral specification like “This function turns a list into its sorted equivalent.” Best wishes, Wolfgang