Home » forums » LtU Forum

Metrics or formailizations of "local reasoning"?

Often in modularity discussions the concept of "local reasoning" is discussed, and it's always assumed we want to make it easier, as a tactic for in turn making it easier for programmers to keep programs in their head. 'Local' to me implies that we have some notion of distance, and I'm curious what work if any has been done on measuring that distance. I've seen lots of claims about X or Y language feature reducing the ability to engage in local reasoning, but no attempts at quantification, without which I don't understand how the languages can be properly compared. Papers, links to prior discussions, etc. appreciated.

By dataangel at 2009-12-30 22:58 | LtU Forum | previous forum topic | next forum topic | other blogs | 3926 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Perhaps a trite answer, but

Perhaps a trite answer, but it is often an obvious binary question when you look at the formal semantics: is it a question of the lexical environment or store? Dynamic or static? Shadowed or not? Open or closed term? This appears in both general semantics (with different flavors in operational vs denotational) and more restricted interpretations like type systems.

Quantifying it beyond 'yes' or 'no' is an interesting question (and I'd lean towards thinking about denotational semantics if you do want a metric..).

Unclear from all of this is when we talk about a desugaring or global transformation. E.g., state-passing or continuation passing style vs. having continuations in the semantics. I've been thinking about the meaning of mining (and thus quantifying) such patterns for awhile but have nothing good to point you to beyond silly stuff like information theoretic notions / UTMs and NLP.

By lmeyerov at Wed, 2009-12-30 23:26 | login or register to post comments