3 ms·

To truly encode it you need dependent types, but even then you might get a beautiful specification and a program that is proved to satisfy it, only to find that

• codygman 11y ago
  I mostly agree, but I'll say (usually at the cost of more complexity upfront) you can encode quite a bit of logic into Haskell's type system. But yes, you can easily create a beautiful specification for the wrong thing. I think that is worlds better than accidentally creating the right thing. We want precision right? Not to brute force try solutions until one seems to work that blows up later?
  • iamcurious 11y ago
    you can encode quite a bit of logic into Haskell's type system You are right, it has limits, but we can push those limits quite a bit. A nice trick is to avoid Bool and look for richer types instead. For instance, avoid <= :: a -> a -> Bool. Use compare :: a -> a -> Ordering. We want precision right? Not to brute force try solutions until one seems to work that blows up later? Not sure. I like precision. I like to study it, I like to be able to use, I hate when other people don't use it, but I have come a long way building the discipline to use it consistently. Some days I still choose nasty hacks.