Lambda the Ultimate

Like Chris, I read it after Paulson's book, and thought I might get deeper insights into the language, but I think I ended up more confused. ;-)

This bleeds into another thread somewhat, but I think the difficulty is those darned HOTs again. It seems that if you are used to thinking operationally (as most programmer's do), having to reason through the type logic adds just a bit too much cognitive load for it to be easy. (YMMV)

As for functors, I found the easiest way to deal with them was to think of them as "structure factories" and leave it there. Once again it seems that when you are up to your elbows in programming, they add just a little too much to the cognitive load to be easy.

It seems that each of the Little Xer books tries to teach a different "essential" programming concept. Schemer: "The goal of this book is to teach the reader to think recursively." Seasoned Schemer: "covers higher-order functions in more depth than The Little LISPer/Schemer and introduces set! and continuations." Mler: "type-directed functional programming". And if that's not enough, with have A Little Java: that "covers the essence of class-based, object-oriented programming...uses a data-driven approach...design patterns like the interpreter pattern, the composite pattern, the visitor pattern, and the factory method pattern."

Funnily enough, I picked up The Little Schemer this weekend. I like the pedagogical style, but wonder how well it holds up when you get into meatier topics - have to buy The Seasoned Schemer to find out.

I wonder what "essential" programming concept The Little Haskeller would teach? Laziness, possibly? Then you could have The Little Erlinguist for concurrency...

Algebraic manipulation, obviously...

Really? I almost never do exercises in programming books. They're so boring!

I used to try to do exercises in important books, but that has been very counterproductive for me. I put SICP back on the shelf for a year because I got so bored with the exercises early on. I still have TAOCP on the shelf after getting bored of the mathematical preliminaries, though a quick brose ahead makes that material look deferable.

I like to just read right through and skip over the exercises. That's really enjoyable, and although you miss a lot of depth you do pick up the big ideas. I find this makes many "hard books" into "fun books". After reading a good book in this way I always end up finding (or contriving) some practical application for its ideas within a year or so, and that takes me purposefully back through the material in more depth.

I note this because I've seen friends also putting SICP aside after getting bored early on. I think there's a little psychological barrier stopping people from just skipping anything that's boring on the first reading, even though it can often be the right idea :-)

That said, The Little Schemer is different for me, since the exercises are so nicely woven into the flow of the book.

(Or maybe my real problem with exercises is that I do all my reading on the bus to work, and it's a bit awkward to break out a pencil and paper there :-)

(Oh, you said examples, not exercises. In that case, disregard everything I just said! :-)

I think the thing to remember about most texts is that they tend to be aimed at being assigned for courses (a captive market;-)) rather self-study. Since instructors want ready-made assignments and test questions, there tends to be more exercise material than one person can use and no solution sets.

For this reason, I long ago came to the conclusion that a self-studier of mathematical and PLT texts MUST skip most of the exercises if they ever want to finish the book. My solution tends to be to pick a few questions that I find interesting and only do those, just to test my understanding, and to see some practical ramifications of the material.

If I get bogged down in a question I thought looked interesting, I just skip it and move on. If I really haven't understood something important, it will become clear (or, rather, unclear ;-) ) as I proceed with later sections.

I agree this is one of the brilliant things about the "Little" series: they find a way to meld the exercises with the text, so that complex ideas "sneak up on you" instead of making you run away when you spot them at 100 paces.

A function maps some input data objects to (usually) one output data object. A functor maps some input data TYPES (usually just one) to an output data type. Most typically, a functor is a "factory" for producing specific instances of data types (structures in ML terminology, so the type can include functions, type definitions, etc.), given some input data type (structure).

For instance, let's say you wanted to implement a Set structure, but you wanted to have the freedom to use different internal representations for the set (e.g. hash tables, linked lists, arrays). To accomplish this, you would define Set as a functor, and then you would define a HashTableSet, LinkedListSet, and an ArraySet as instances of that functor given the HashTable, LinkedList, and Array types. In pseudo-ML:

HashTableSet = Set(HashTable)
LinkedListSet = Set(LinkedList)
ArraySet = Set(Array)

Of course, there's more to it than that. You need to be able to define all the non-instantiated parts of the Set data type in terms of the corresponding parts of the HashTable etc. structures.

Also note that all this is done at compile time. Functors are like a more well-behaved and less efficient version of C++'s templates.

Mike

• Is map f . map g = map (f . g) ?

  Yes!

• But how can we be sure?

  We can try a few examples. We can also try to find a proof.

• How can we prove equations like this?

  We can do algerbraic manipulation, use universal properties. we can also use induction.

• Will induction work?

  Yes!

• On what will we do the induction?

  The hidden list argument, of course.

• The base case of the induction is map f . map g [] = map (f.g) []. Does this hold?

  Yes!

• What is the induction step?

  map f . map g xs = map (f.g) xs implies map f . map g (x:xs) = map (f.g) (x:xs)

• Can we show that this holds?

  Yes! Do it!

• So have we shown tha map f . map g = map (f . g) for all lists

  No. Our proof works on for finite lists!

• Can we fix that?

  Yes! But first we will have some Pizza. You should too!

I find reading them quite boring, and when I finally get to the sections that are new to me, I don't find the qustion/answer approahc very enlightening.

Linear text works better for me.

However, this style may be just the right thing for showing step by step proofs, and program transformations!

I would really like to see this fleshed out to full length; maybe Friedman and Felleisen will give you franchise rights, if you ask them nicely. (And bribe them with Pizza) ;-)

No, no. This time the bell wasn't called for. It was a "Ha Ha only serious" kind of thing.

Marc, I think your cognitive factors are like a black hole: nothing can escape it, not even illumination.

And it recalls an argument of Popper's, to do with irrefutability.

Perhaps we should coin a variation on Godwin's Law too: "As any LtU discussion grows longer, the probability that some idea will be dismissed by invoking cognitive or human factors approaches one."

And the corollary: "The surest way to neutralize a discussion on programming languages is to suggest that an idea is infeasible because it increases cognitive burden." (I need not point out that every unfamiliar idea implies increased cognitive burden in the short run.)

No one here is trained in cognitive science or human-computer interfaces. No one can field a cognitive factors argument. Every argument based on some supposedly looming but nebulous cognitive danger puts the subject of disagreement into rhetorical limbo, where everyone must fear it and no one can retrieve it.

I'm not going to participate in those kinds of threads anymore, because it's not productive. I encourage the rest of you to do the same. Let's try to keep things factual or falsifiable.

I understand your concern about falsifiability Frank, but I think if we limit ourselves to those aspects of our experience that are objectively verifiable, we won't have much left to talk about.

I don't mean this facetiously; I think it is simply one of the core epistemological challenges of understanding the world.

The issue of human factors is a core issue in PLs to the extent that they are tools to be used by humans to accomplish practical tasks. As with anything else, we can study them theoretically as a phenomenon unto themselves, and personally I find this interesting as well, but, as a programmer, I'm also interested in how they are used and why.

My "cognitive load" argument is not intended as an objective statement of falsifiable fact, but a good-faith expression of my experience. Here I am, someone who enjoys spending time working with very difficult theoritical material (abstract math, mathematical PLT) for fun, and who has many years of experience as a programmer using different languages and levels of abstraction, and I find it harder to program using HOTs.

It is entirely possible this is a strange defect of my brain or experience, but I don't seem to be the only one who has experienced this. (see Benjamin Pierce's presentation, recently mentioned on LtU)

A possible response to me is to say "Hmmm. In my experience, I find that building large software systems is just as easy with HOTs; I never have problems understanding them" or "HOTs are just so valuable a tool for software that I struggle along with them anyway, and here are some ideas I have for making them easier to use." Either could lead to a productive discussion without necessarily being falsifiable.

I'm not going to participate in those kinds of threads anymore, because it's not productive

If you stop participating, I for one will miss hearing what you have to say. To me a thoughtful, reasoned, good-faith discussion of different points of view is always productive, though seldom objectively resolvable.

I know how you feel. I am also frustrated when discussions start to be of the form "I find it difficult at the moment, ergo it is too difficult for programmers."

However, we shouldn't dismiss human factors. They exist, and can be important. We should exercise some restraint, and try to concentrate our efforts on real PL research.

There is a reverse argument that many feel frustrating too: "Our research is really fruitful in this area at the moment, so this should be more important for programmers." ;-)

But more seriously, I'm not sure if you are characterizing arguments other than mine with that summary sentence, but whether that is the case or not, it seems that what you are expressing frustration over is a clash of premises.

One premise says (maybe): "The purpose of PLT is to find more elegant and intuitive mathematical models to reason about PLs and to prove them to have certain properties."

The other says: "The purpose of PLT is to find simpler and more intuitive ways for programming to be done effectively and safely."

They aren't mutually exclusive but they focus on different things. Each has a subjective component (what is elegant or intuitive, for example), and I don't see how we can discuss these real factors without invoking subjective experience. (e.g. "I find this version of that proof more elegant" or "I find this language feature more confusing than helpful").

Depth of experience may affect the weight one might give to a particular point of view, but that is another matter. ;-)

We should exercise some restraint, and try to concentrate our efforts on real PL research.

I would be interested in your definition of "real PL research". I was under the impression that sociological and "human" factors were part of the range of phenomena you wanted to discuss.

Sure. But I prefer arguments that are not based just on personal introspection..

And to be clear: I wasn't referring to your posts, most of which I find very interesting and informative.

One premise says (maybe): "The purpose of PLT is to find more elegant and intuitive mathematical models to reason about PLs and to prove them to have certain properties."...The other says: "The purpose of PLT is to find simpler and more intuitive ways for programming to be done effectively and safely."

Personally, I don't accept this sort of split. I think these things go hand in hand.

Still, I think that many programming techniques (with formal theory behind them or not) sounded complicated and adding cognitive burden, until people grew more comfortable with them, with experience. Looking back, people say "how could we ever live without X" (some suitable Xs: moudules, static typing, type inference, unit testing, symbolic debugers etc.)

So my approach is to defer the conclusion that something causes undue cognitive burden for as long as possible.

Interestingly, all of those Xs are things that many people still have issues with. ;-)

So my approach is to defer the conclusion that something causes undue cognitive burden for as long as possible.

A reasonable policy. But there is still an interesting question even if you don't accept the burden as "real" or "proven": why do people perceive it to be there? Put differently: what is their mental model of programming that causes them to feel the way they do?

The answer could lead to new pedagogical or theoretical approaches that address the "problem".

why do people perceive it to be there?
Ask for an explanation and people will do their best to generate one for you, even when they can't possibly know - psych 101.

some idea will be dismissed by invoking cognitive or human factors
... and without providing any evidence that there is a significant effect. Testing is for human factors as-well-as TDD.

Is it possible that he had something in mind for "effective" that didn't mean "faster"?

Though I know it is tempting to think that users are just insane ;-), it is possible that they have some unstated value underlying their perception. Getting an idea what that is helps the designer to determine how to address the issue, or even if it is really worth addressing.

That's not objective or properly testable, but few things involving people are. ;-)

Ask for an explanation and people will do their best to generate one for you, even when they can't possibly know - psych 101.

That calls into question their explanation for the phenomenon, not the perception of its existence.

Testing is for human factors as-well-as TDD.

As your CEO example shows though, finding an effective, objective test for human factors is quite tricky.

If our discussions here lead to even some consensus of what to test for in those cases (or if we are even luckier how to test for them), we would have advanced our shared understanding.

tempting to think that users are just insane ;-)
Is it?

As your CEO example shows
Hardly.
The objective test was simple and straight-forward.
As a direct result of the test we changed the menu structure of the product - the product manager and marketing manager had no difficulty seeing from the numbers that the CEO (and everyone else) was faster with the new menu structure.
So the test was also effective.

The more I think about this, the more I like the idea of a Little book about Haskell and algebraic programming. I am not sure if I am the right man for the job, though...

Some time ago I started writing a book about software abstractions (using Ada) with the tentative title of The Little Abstractionist. Alas, that wan't meant to be. Looking back, it seems Ada wasn't a good choice anyway. A high order functional language looks much nicer now. It's not the languages that changed, it's me...

I agree that testing is important here, but I've seen this argument abused... In some cases, someone doesn't like a proposed solution to a problem, so they invoke the "no quantitative evidence" argument to get it dismissed. When used this way, even the person making the argument may be aware that there's really no way to acquire quantitative evidence in a particular case, or any clear picture of what it would look like. (The king said, "Sure, you can marry my daughter the princess... As soon as you bring me a hen that lays golden eggs.")

Even when human factors testing is, in principle, possible and there are clear metrics for success in the domain, there are many cases where the argument still doesn't stand up. While it makes perfect sense in a situation like Isaac's menu structure scenario, it's a lot less clear that it makes sense when we're talking about programming langauges.

Here's one reason: for most of the changes that are of real interest to language designers, the learning curve is quite long, and in some cases, the real outcome can't be seen until an entire community of programmers have become accustomed to a particular feature and developed a way of designing, writing, thinking about and talking about programs using this feature, as well as their own ways of teaching the feature to novices (the way an experienced Java programmer would teach a new programmer to program is very different from the way Java was first presented, when in fact there was no such thing as an experienced Java programmer). Even now, many would argue that the results "aren't in" on many established languages, because the community as a whole continues to refine its understanding. Witness the recent revolution in the C++ community's understanding of templates.

Even if you do have a captive community of programmers and you're willing to invest five to ten years in evaluating the success of your language decisions (Erlang, anyone?), it's still impractical to use testing to explore the design space, since you can really only set up and run one or two longitudinal studies. This being the case, the language designers still need to rely on previously gathered data (of arguable applicability), personal experience and anecdotal evidence, and intuition, at least when deciding what particular areas are likely to be worth exploring.

That said, I'm all for testing on humans, and I too dislike broad unsupported generalizations like, "This feature is just too hard for most programmers." I guess that, in the absence of quantitative evidence, I would always err on the other side and assume that users will understand some feature rather than assume that they won't. If anything, historical evidence shows that programmers are willing and able to learn to do difficult things with difficult tools, as long as there is a community to support them. For the record, my favorite text editor is vim.

You're right, doing so would restrict us to miniscule fields such as mathematics, logic, physics and chemistry. Your remark explains why these subjects have had such a negligible impact on our world.

Here I am, someone who enjoys spending time working with very difficult theoritical material (abstract math, mathematical PLT) for fun, and who has many years of experience as a programmer using different languages and levels of abstraction, and I find it harder to program using HOTs.

It's not so strange. Donald Knuth's favorite languages are CWEB and MIX assembly, and I know plenty of computer scientists and even mathematicians who program exclusively in procedural languages.

One premise says (maybe): "The purpose of PLT is to find more elegant and intuitive mathematical models to reason about PLs and to prove them to have certain properties." The other says: "The purpose of PLT is to find simpler and more intuitive ways for programming to be done effectively and safely."

I agree with Ehud: these go hand in hand. I don't know much about human-computer interfaces beyond the popular science literature, but one thing I do know is that it is important for a user interface to be consistent, and that a user be able to develop an (elegant and) intuitive model of the application in his head. These are precisely the qualities which the mathematical approach to PLT optimizes.

To me a thoughtful, reasoned, good-faith discussion of different points of view is always productive, though seldom objectively resolvable.

There are questions which can be settled objectively, and questions which cannot be. Both sorts are important, but it is important also not to confuse them, because frequently a question of the second sort depends on answers to questions of the first sort. What I'm sick of is people shoving everything into the second category and pontificating endlessly about it like critics, because then nothing ever gets done.

it's still impractical to use testing to explore the design space
Not really. It is practical if we are interested in testing qualities of a specific design. Over the last decade that approach has become known as discount usability engineering.
The approach you described seems closer to basic scientific research.

most of the changes that are of real interest to language designers
Sorry, I don't have the experience to know specifically what those things of real interest are.

“When you can measure what you are speaking about, and express it in numbers, you know something about it; but when you cannot measure it, when you cannot express it in numbers, your knowledge is of a meager and unsatisfactory kind: it may be the beginning of knowledge, but you have scarcely, in your thoughts, advanced to the stage of science.”
William Thompson, Lord Kelvin, (1824–1907)

Hmmm. For the first two, I think you have conflated objectively verifiable with logically consistent. If two people disagree about the axioms they can't agree on the truth of the rest of the structure.

Large swaths of physics (notably quantum level phenomena) are in a similar boat, as either not directly observed or in principle not directly observable. Even physicists disagree if they are "real" phenomena or merely convenient fictions.

Chemistry is doing much better here, but I can't see how to apply it to PLT. ;-)

I know plenty of computer scientists and even mathematicians who program exclusively in procedural languages

Do you think this is necessarily mere preference, or that there is some potentially objective reason why this is so?

If we insist on the former, we might as well give up asking questions like "Why is language X more popular than Y?" or "Is PL X better than Y?" because all criteria (axioms of evaluation, if you will) will ultimately be subjective.

to develop an (elegant and) intuitive model of the application in his head. These are precisely the qualities which the mathematical approach to PLT optimizes.

I have to contend that "intuitive and elegant" are contextually and subjectively determined to some extent. What is intuitive to a PhD in Math may be completely unintuitive to someone who is not. In practice, the kind of consistency one looks for in UIs does not seem to be identical to that which one seeks in a mathematical theory.

What I'm sick of is people shoving everything into the second category and pontificating endlessly about it like critics, because then nothing ever gets done.

While I sypathize that blogging can be like that ;-), I'm still at the point where I'm trying to flush out my own (and others) hidden assumptions about PLs.

When confronted by, say, Python enthusiasts who proclaim the superiority of their language because of its "dynamic properties", I can simply write them off as deluded or ignorant or as simply having tastes that are irreconcilable with mine.

But, as Ehud prefers to defer appealing to "cognitive burden", I prefer to defer setting the "Bozo bit" until I have satisfied myself that I have an adequate model of their "axioms of evaluation" (or even my own).

And what better place to find out what those are than through LtU Discussion? ;-)

Ain't my approach. I try to analyze the language properties, to see how they can be modeled, examine theiry safety etc. That's a big part of my research agenda.

I can tell when I am not successful. That doesn't mean, of course, that I should agree to accept unsupported theories strongly held by others...

The language properties you care about, or the ones that the proponants put forward? ;-) Safety, to use your example, doesn't seem to have a high priority for many people. How do you model the trade off between safety and utility? Remember that the safest program is the one that terminates immediately without doing anything. ;-)

That doesn't mean, of course, that I should agree to accept unsupported theories strongly held by others...

I'm not suggesting that anyone accept or agree with such theories, but rather that it is worth understanding the premises behind them and the point of view they represent. I guess you could say I'm a fan of the Socratic method. ;-)

It seems you are going out of your way to be provocative. But it doesn't work on me this time...

I know what they want to achieve. I also know that they don't always realize the tradeoffs.

Your recent posts are in the spirit of those that claimed they have proven Fermat's last theorem. When they were seen as crackpots they claimed that this just proves that the establishment isn't willing to accept their radical new ideas. The next step (let not go there in our debate) was to invent consipracy theories...

I think it's much better to discuss concrete issues. Give a design, give its properties, rank their importance if you want. Then we can compare designs (in competeing languages), and see how they stack up.

I, for one, haven't seen to many convincing arguments that show that dynamic type checking help achieve most of the qualities ascribed to so-called dynamic languages. However, it is quite easy to see that some statically typed languages have weak type systems, that indeed make some designs harder (see my paper on abstraction breaking).

Not for the sake of it, no. My intent has been to show that everyone accepts as objective some things that are in fact subjective. If that is starting to seem like provocation, perhaps I should consider my point past being made. ;-)

When they were seen as crackpots they claimed that this just proves that the establishment isn't willing to accept their radical new ideas.

What was that about being provocative? ;-)

I don't have any radical new ideas to sell to the establishment (I'm not even sure in this case who the establishment would be ;-))

I merely have a dilemma: after many years of interest in, and study of PLT, and much more and broader experience of being a programmer (in both amateur and professional capacities) I believe that both PL theory and programming practice have valuable lessons to give about the design and selection of PLs, but that sometimes they are not the same lessons (or at least not ranked the same).

It is like the old joke: "In theory, theory and practice are the same, in practice they're not".

Unfortunately, I can't think of a way of proving this, even in principle. I can only appeal to my subjective experience and that of others. And I'm not sure how to even discuss the evaluation of PLs (distinct from the description of them) meaningfully without considering both domains.

Give a design, give its properties, rank their importance if you want. Then we can compare designs (in competeing languages), and see how they stack up.

If I haven't burnt myself out on posting, I'll give that a shot in another thread. ;-)

see my paper on abstraction breaking

I'll take a look. Thanks, Ehud.

No, I think it is you who are conflating `objectively' with `empirically'.

If two people disagree about the axioms they can't agree on the truth of the rest of the structure.

Irrelevant. What they agree on is an implication: given such-and-such hypotheses, we must conclude so-and-so. The truth or otherwise of the hypotheses is a separate question, and is hardly ever an absolute anyway. For example, do you grant the `truth' of the axioms for a monoid? The question is absurd. The proper question to ask is rather, in category C, can object X be equipped with the structure of a monoid?

The Hilbertian preoccupation with finding a universal set of postulates, a universal foundation for mathematics, was abandoned after Gödel. These days mathematics focuses on the question of what theorems can be proved from a given set of postulates, not on the choice of postulates themselves.

Large swaths of physics (notably quantum level phenomena) are in a similar boat, as either not directly observed or in principle not directly observable. Even physicists disagree if they are "real" phenomena or merely convenient fictions.

So what?

Look, I'll just cut to the chase: Do you think that anything is objectively verifiable? (If not, we have no common ground, and you can go argue with Alan Sokal.) And, do you think that objective analysis of phenomena has had a significant impact on our world?

Frankly, I think you are arguing yourself into a very deep hole. Eventually you will need something like "cogito ergo sum" do dig your way out...

Do you think this is necessarily mere preference, or that there is some potentially objective reason why this is so?

What I think the reason is doesn't really matter, but I will give you my opinion. I think some reasons are that, a) compared with professional programmers, they do relatively little programming so the choice of language does not affect them much, b) there is a relative scarcity of accessible educational material on `declarative' languages, and the implementations are not as well-supported or complete as those of procedural ones, c) there is some prejudice and they are infected with `new frontier' syndrome, d) like Dijkstra says, they derive enjoyment out of not quite knowing what they are doing, e) popular opinion has already convinced them to abandon the idea that programs can ever be correct by design, and f) many of them have no clue that declarative languages even exist.

If we insist on the former, we might as well give up asking questions like "Why is language X more popular than Y?" or "Is PL X better than Y?" because all criteria (axioms of evaluation, if you will) will ultimately be subjective.

The popularity issue is certainly subjective in the sense that likes and dislikes depend on the person. If you want to attack this issue in a rational way I recommend getting a degree in marketing. Frankly popularity issues don't really interest me as a topic of discussion, and so I welcome your suggestion to `give up' on it.

I do agree that the question, `Is PL X better than Y?', is ultimately subjective. But I think there are a few things that many people can agree on, which can be measured objectively: X is better than Y if X is more modular, if X lets me express declaratively more facts (such as invariants) I know about the program, if X can be compiled more efficiently, and so on.

That is why, in particular, when there exists a full and faithful embedding of Y into X but not of X into Y, I think it is a very powerful argument that X is better than Y.

I have to contend that "intuitive and elegant" are contextually and subjectively determined to some extent.

Certainly: they're your own words! Otherwise I would not have used them. :)

Ehud: When they were seen as crackpots they claimed that this just proves that the establishment isn't willing to accept their radical new ideas. Marc: What was that about being provocative? ;-)

If you think this is provocative, you must still be a Usenet virgin...! :)

I believe that both PL theory and programming practice have valuable lessons to give about the design and selection of PLs, but that sometimes they are not the same lessons

No one disagrees with that. What I often disagree with, though, is the way in which observations gained in practice are generalized into theories, and the way in which theories are applied in practice.

It is like the old joke: "In theory, theory and practice are the same, in practice they're not".

So stop using the wrong theory, or start practicing the right one.

That is why, in particular, when there exists a full and faithful embedding of Y into X but not of X into Y, I think it is a very powerful argument that X is better than Y.

This is not always the case as I reject the concept better when stated without context. For example, consider my reply to your demonstration of implementing a dynamic PL in a static one. Using JavaScript on top of C++ was better for me in the context that it allowed me to limit the functionality available to the JavaScript programmer. Yes, these limits made it better, because I was using JavaScript for a very particular purpose (app customization) and need strict control over what could, and could not, be done.

So if there exists a full and faithful embedding of Y into X but not of X into Y, but using Y makes Z possible a lot more easily (or securly, etc) than using X, Y is still better for Z.

Do you think that anything is objectively verifiable? <snip> Frankly, I think you are arguing yourself into a very deep hole. Eventually you will need something like "cogito ergo sum" do dig your way out...

I'm not a nihilist or sollipsist or any such, but a pragmatist. A very summary view of my position is that to "objectively verify" a position with someone else you have to agree what the terms of the discussion are (the axioms and proof theory if you will). You can of course reject some else's premises as nonsense, but then there is no basis for objective verification with that person.

That is why, in particular, when there exists a full and faithful embedding of Y into X but not of X into Y, I think it is a very powerful argument that X is better than Y.

The devil is in the details here. If the embedding obscures rather than illuminates the basic properties of the embedded system, this might not be that great. Having read Ehud's paper (as well as others) recently, I have been trying to come up with a more principled model of "complicated" that could be used to weed out such situations. I'm still working on this. ;-)