I think there are philosophical reasons why people prefer inference rules over working with sets. Many people work or have worked in a context of constructive l

I think there are philosophical reasons why people prefer inference rules over working with sets. Many people work or have worked in a context of constructive logic, as constructivism comes in naturally when you consider computability. Now, implication is a far simpler concept than sets. Implication is modelled by cartesian closed categories, while for sets one needs additional structure, e.g. toposes. So I suppose the fact that inference rules are preferred over pattern matching and sets has to do with them being percieved as being based on simpler principles. Of course, all this is a matter of taste and for particular applications like HM it doesn't make any difference at all which notation to use. I don't want to defend the rule notation too much; it takes up a lot of space in papers and if you have something better then fine. But maybe that explains why people prefer this notation.