> They are "reinventing a run-time type checker" and prefer it that way because it allows increased expressive power at the cost of delayed verification. Well,

> They are "reinventing a run-time type checker" and prefer it that way because it allows increased expressive power at the cost of delayed verification. Well, to me "delayed verification" is worth nothing. There is an almost unbounded infinity of program states. I want proof before I run the program. (That's, like, the point, man! I'm not going to send up a space shuttle and just count on "oh, well, our error recovery is great and we saw no errors during testing anyway". To quote a great comedian: "Are you having a laugh?") > So you don't actually know how to do it, but assume that you can. Oh, come on, be a little more charitable. I don't know, but people in the DT community know and will tell you... at length how to do it. > By the way, you probably want linear types in order to encode state machines in the type system in a natural way, which Haskell does not have. Indeed it does not... but I must say I don't miss them that much for all practical purposes. If what you want to do is encoding state machines and prove things about said machines, then you probably want an even more specialized language. I'm OK with that. I'm not OK with saying: "Can't be done in language X, therefore all effort at static verification is futile." So there.