Vincent Gable’s Blog

There are a lot of problems that are, in theory, incredibly difficult – but because the difficult cases are very rare and rather contrived, they’re actually very easy to solve. Two examples of this that I find particularly interesting are both NP complete. Type checking in Haskell is one of them: in fact, the general type inference in Haskell is worse that NP complete: the type validation is NP-complete; type inference is NP-hard. But on real code, it’s effectively approximately linear. The other one is a logic problem called 3-SAT. I once attended a great talk by a guy named Daniel Jackson, talking about a formal specification language he’d designed called Alloy. Alloy reduces its specification checking to 3-SAT. Dan explained this saying: “The bad news is, analyzing Alloy specifications is 3-SAT, so it’s exponential and NP-complete. But the good news is that analyzing Alloy specifications is 3-SAT, so we can solve it really quickly

—Mark Chu-Carroll (aka MarkCC