11 ms·

Could you expand on your definition of "properties of interest"? I think Haskell's type system satisfies your list of requirements.

• pron 11y ago
  > I think Haskell's type system satisfies your list of requirements. :) Haskell doesn't even come close. Haskell's type system is pretty much defined to be any property that happens to be inferrable by the (extended) HM algorithm. It's like: "we'll prove what we easily can" rather than "let's prove what's most useful". Sure, it may be useful in some (or perhaps many) circumstances, but it's far from the set of properties I think anyone would list when asked "what properties would you most like to verify about your program?" For example, the two most basic tests for any formal verification system is verifying a sorting algorithm (like, say, QuickSort) and verifying a distributed algorithm (like, say, Paxos). Haskell's type-system fails to do both. Again: it cannot verify the two most common examples that people want automatic verification for. In fact, it is even too weak to verify that the monads it so depends on are actually monads. Still, it places a non-negligible burden on the developer that many would deem substantial or even onerous. And because types place some burden on the developer, you can then ask whether the set of verifiable properties is worth it or not (BTW, that any form of formal verification requires effort is pretty much a given; if it didn't, that would be a violation of the halting theorem). OTOH, richer type systems (that include dependent types) can no longer infer everything, and they become (much) harder-yet to use. Here are some examples of properties of interest: 1. When a request arrives at my server, a response (either a result or an error), is always produced within a given time frame. There can never be deadlocks, livelocks or starvation. 2. X and Y are two columns in my data table that must always satisfy certain invariants, and must never be observed to violate those variants. 3. My O(n) selection algorithm is correct. 4. My (sorting) algorithm requires O(1) space. 5. When a user inputs "X" the system will (or will-never) output "Y" within 5 seconds. There are many, many more. I picked those because there are formal verification tools today that can verify all those properties (or at least many interesting instances of them). Of course, some proofs would require your computational model to be non-Turing complete, because the halting problem is real...
  • tel 11y ago
    I think the very most common property of programs I or anyone ever deals with is handily covered by Haskell's type system: "do these two (often complex) things fit together?" The other properties you mention are great! I'd love to verify them too. We'd be better off if those tools were widely used. But that's far from staying that what we have today isn't fantastic.
    • pron 11y ago
      > I think the very most common property of programs I or anyone ever deals with is handily covered by Haskell's type system: "do these two (often complex) things fit together?" That is indeed very common, but it is neither the most important (it might be, but that requires evidence) nor is Haskell's particular blend of proof vs. burden necessarily the best. You could have said the same about Java, C#, Go or C, each with their own limited type "richness". > We'd be better off if those tools were widely used Formal verification tools that are able to prove many of the example I listed (or interesting-enough special cases) are far from being in wide use in the industry in absolute terms, but they are certainly in wider use than Haskell (in spite of the latter's popularity among bloggers), at least when it comes to large, complex software, which is where verification is most valuable anyway. Fujitsu have used JPF to verify a 1MLOC Java program[1], Amazon use TLA+ to verify/specify most (all?) of their AWS services (written in Java), some are quite complex[2], Esterel (or, rather, its descendants) is used by various realtime systems[3], and Intel uses TLA+ and/or internal verification tools to verify components in its processors. Each of those alone has seen more real-world "tough" industry usage than Haskell. AFAICT, those tools are in wider use than Haskell in academia, too (aside from PL research, obviously), where they're sometimes used to verify concurrent/distributed algorithms (and in at least one famous case, prove the incorrectness of a much-lauded algorithm[4][5]). It is, however, true that type-based verification tools (like Coq) have seen even less use than Haskell (they're basically unused in the industry) and other proof assistants are rarely used (a notable example is Isabelle, which has been used to verify the seL4 kernel, but AFAIK Isabelle isn't type-based, but, like TLA+, uses set-theory). Even in academia, use of type-based proofs is very rare (virtually nonexistent outside PL). [1]: http://javapathfinder.sourceforge.net/events/JPF-workshop-050108/SymbolicJPF08.pdf http://javapathfinder.sourceforge.net/events/JPF-workshop-05... [2]: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-s... [3]: http://www.esterel-technologies.com/industries/ http://www.esterel-technologies.com/industries/ [4]: http://www2.research.att.com/~pamela/chord-ccr.pdf http://www2.research.att.com/~pamela/chord-ccr.pdf [5]: http://brooker.co.za/blog/2014/03/08/model-checking.html http://brooker.co.za/blog/2014/03/08/model-checking.html
• deleted 11y ago
  [deleted]