Except in the complexity gymnastics and the fragility of the conclusions. Humans can't do large scale complex brain gymnastics - that's why abstraction exists - if your proof process doesn't abstract (and in the C case you need to know *everything* about *everything* and have to "prove" it all in one go and that proof will not survive a single change) then it isn't feasible.
Haskell gives you the means to manage the complexity - and grasping complexity is humanities current challenge... Neil On 28 Jul 2012, at 05:43, damodar kulkarni wrote: > > > So a language is referentially transparent if replacing a sub-term with > another with the same denotation doesn't change the overall meaning? > But then isn't any language RT with a sufficiently cunning denotational > semantics? Or even a dumb one that gives each term a distinct denotation. > > That's neat ... I mean, by performing sufficiently complicated brain > gymnastics, one can do equational reasoning on C subroutines (functions!) too. > > So, there is no "big" difference between C and Haskell when it comes to > equational reasoning... > > > Regards, > Damodar > > > On Sat, Jul 28, 2012 at 1:47 AM, Alexander Solla <alex.so...@gmail.com> wrote: > > > On Fri, Jul 27, 2012 at 12:06 PM, Ross Paterson <r...@soi.city.ac.uk> wrote: > On Fri, Jul 27, 2012 at 07:19:40PM +0100, Chris Dornan wrote: > > > So a language is referentially transparent if replacing a sub-term with > > > another with the same > > > denotation doesn't change the overall meaning? > > > > Isn't this just summarizing the distinguishing characteristic of a > > denotational semantics? > > Right, so where's the substance here? > > > My understanding is that RT is about how easy it is to carry out > > _syntactical_ transformations of a program that preserve its meaning. > > For example, if you can freely and naively inline a function definition > > without having to worry too much about context then your PL is deemed > > to possess lots of RT-goodness (according to FP propaganda anyway; note > > you typically can't freely inline function definitions in a procedural > > programming language because the actual arguments to the function may > > involve dastardly side effects; even with a strict function-calling > > semantics divergence will complicate matters). > > Ah, but we only think that because of our blinkered world-view. > > Another way of looking at it is that the denotational semanticists have > created a beautiful language to express the meanings of all those ugly > languages, and we're programming in it. > > A third way to look at it is that mathematicians, philosophers, and logicians > invented the semantics denotational semanticists have borrowed, specifically > because of the properties derived from the philosophical commitments they > made. Computer science has habit of taking ideas from other fields and > merely renaming them. "Denotational semantics" is known as "model theory" to > everyone else. > > Let's consider a referentially /opaque/ context: quotation marks. We might > say "It is necessary that four and four are eight. And we might also say > that "The number of planets is eight." But we cannot unify the two by > substitution and still preserve truth functional semantics. We would get "It > is necessary that four and four are the number of planets" (via strict > substitution joining on 'eight') or a more idiomatic phrasing like "It is > necessary that the number of planets is four and four". > > This is a big deal in logic, because there are a lot of languages which > quantify over real things, like time, possibility and necessity, etc., and > some of these are not referentially transparent. In particular, a model for > such a language will have to use "frames" to represent context, and there > typically is not a unique way to create the framing relation for a logic. > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > > > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
