Showing posts with label reasonning. Show all posts
Showing posts with label reasonning. Show all posts

Wednesday, November 4, 2009

Bad Separation of Concerns

In the course of my master's, I have to attend a seminar and prepare one talk. Last week, the talk I listened to was about using pattern matching in object oriented programming languages. I thought, as the talk went on, that all the yardstick they took to evaluate the design of their language construct was all wrong. It struggled, in my opinion in vain, to improve the expressiveness while retaining the best possible performances and remaining "concrete". In that respect, I tend to take for granted the necessity of expressing precise specifications with every piece of code. This means that, for me, the most important is that my specification language be expressive enough, but still very simple, to allow me to reason about my problems and my implementation language be as simple as possible and allow me to express any algorithm I wish. In my experience, the specification language should involve as little operational elements as possible for simplicity. As for the implementation language, it should be possible to implement it on any reasonable architecture. Before I'm objected that it is not customary in industry to use precise specification notations or to keep multiple representations, at different degrees of abstraction, of a single solution, I have to point out that this is an academic result and it does not have to follow industrial customs. Actually, I would go one step further and state that, if, in academia, we wait for techniques to become widely adopted before using them, we are lagging behind and risk doing no more than producing more of the same. Academia being more remote from the market place than industry are supposed to be less affected by the political issues that keep industry behind the state of the art. And this is not badmouthing the industry: it is understandable that they have more concerns than only technological ones. Let's get back to the paper. In their design, they seemed to tackle both problems of expressiveness and implementation at once and the result was not pretty. For example, in their pattern matching, they had to take into consideration that the evaluation of the expression (which, in their case, is an absolute necessity) they were dealing with could very well have side effects and this was an important concern of theirs. I think that this possibility was popularized by C and I think this is an important set back with respect to allowing programmers to think about their programs. I think, already, the discipline of separating queries from commands, which is part of Eiffel's style, is much better in this respect. They also had to deal with constructors in order to match objects like you would in Haskell. This is very ugly. Pattern matching is a very elegant way of writing expressive specifications but object creations do not fit in it. This is because an expression creating an object has an implicit reference to memory allocation and it can't be dissociated to it. People can't forget that the object has a memory representation and that a comparison in the context of pattern matching will have a given cost. I prefer to use mathematical expressions to express the value contained by the object and allocate the object only if necessary.
Aside In a recent programming experiment where I derived my code from its proof of correctness, I was parsing a string and, since all the properties of a language can so elegantly be formulated in terms of strings of character, I used strings to represent the state of the computation. I had my input string S, the processed string x and the left over string z and they were linked by the invariant:
S = x ++ z
with ++ the string concatenation operator. At each iteration, I split z in two parts such that
z = [ y ] ++ w
and scanning one character was encoded as:
x, z := x ++ [ y ], w
If you can't help yourself and have to imagine the memory footprint and performances of this algorithm, you might be scandalized that this is really inefficient. This is not meant to be executed as such; it is only a very simple way of understanding defining what the algorithm does. With one data refinement, I went to a representation where the use of memory is limited to the array representing the input, an integer index indicating which character y is and two booleans to represent the acceptance state of the algorithm. There is no efficiency problem with that, and my proof of correctness and my proof of data refinement are very simple and I consider them the clearest documentation for the algorithm.
end of aside
In summary, I think the right way of seeing that problem is:
Pattern Matching is a power way of associating properties or code with the shape of the data and we need to be able to express it. Since we can use it with code, it would be important to have programming techniques to make the executable, that is, techniques usable by a programmer to transform a specification using pattern matching into executable code implementing it. If the methods are especially effective and simple, we could have it implemented in our compiler but this is far from being a design consideration for the construct.
* * *
More recently, in my compiler design class, we were presented a research programming language which is said to be "relationship-based". I think the idea is a good one: they factor the inter-class relationship out of classes to treat them as separate modules. The question whether each such relationship deserve its own module is worthy of debate but, for now, what bothers me is that they treat it as a programming language construct, that is to say they keep an "implementability anchor" in their heads while they design the notation. One of the consequence is that they will refrain from adding anything for which they aren't sure they can compile it automatically. I would rather see this emerge as a specification structuring artifact and see some programming techniques emerge in connection to it so that the most common one can be implemented quite straightforwardly. For the rest, it's open to experimentation and, in all cases, a case by case implementation would allow optimization that systematic compilation wouldn't be able to do.
I think the big problem here is still the taking of current practices as a guideline for academic research: "since programmers don't write specifications, we won't provide a means to write good specifications even though progress would require it". I put it in my "more of the same" bin, look at the original ideas and forget about the language. Actually, I will do so when my semester is over.
Simon Hudon
ETH Zürich
finished on November 18th

Saturday, September 5, 2009

Collective Knowledge

At the moment, I have a few drafts I am writing but they are not progressing very fast and I am offering this short reflection. Looking around and reading different kinds of research, I can't help but feel that there exists a hierarchy of collective knowledge. Science is part of that hierarchy but it is not the whole story. As somebody who is strongly mathematically inclined, I have a tendency to view formal mathematics as the only means for expressing one's understanding but this position does not hold water. Since I am also very interested in methodology, namely, how we program and how we do mathematics, I have to have considerations for human activities and those are particularly hard to formalize and one might wonder what need we have of formalizing them. It must be honestly revealed that the activity of formalization demands tremendous efforts which are not carried out merely for the beauty of formal theories (although, many don't need much more motivation for doing it). The point is that, at any time before embarking on a formalization project, it is worth it to wonder if it is worth embarking on. On one hand, there is a class of programming languages, of which C++ and PL/I are nice representative, for which the formalization is not worth the effort because they are so complex and there documentation is so ambiguous that the formalization amount to reinventing them. Also, while reinventing them for the sake of formalization, for survival's sake, one should have the reflex of questioning every design decision before deciding to adopt them and, doing so, one would not end up with C++ or PL/I but with a language à la Wirth. If we carried that judgment to a further conclusion, it can also mean that they are not worth using either. On the other hand, there are subjects which are worth studying but the gain of a formalization is not immediately obvious. We have other tools than formalization to be rigorous and precise in our discourse and should not neglect them (to name only one: we have our natural language for which an exceptional mastery can do wonders). Once the benefit of formalization is seen, though, one should not hesitate. At the moment of writing, I am thinking about the general literature about programming methodology (aka software engineering). I have the feeling that although some publications concentrate on giving examples of the use of a particular method, some succeed at being very rigorous by being modest and accepting that they are merely working with one example. Also, their rigor seem to rely on the analysis of their example, of what helped and what did not. On the hand, some very disappointing papers on the topic try to be more rigorous by building a tool, having a handful of programmers use them, measure (in some vague sense) the improvement in their productivity and publish the statistic. Without a theory to compare those numbers to, they are meaningless and I can't help but see it as another instance of the general hype around statistic which I would summarize with "a number is better than no numbers at all". Simon Hudon Zürich, September 5th 2009

Tuesday, August 18, 2009

On Credibility

I just had a conversation on Skype with my mother and I made an interesting reflection while seemingly lecturing on our attitudes toward great authors. I was talking about the way Edsger Dijkstra was prejudiced and said that I found it too bad because he was otherwise very smart. And then I thought back on the period where I had not realized the prejudices that he had and wondered what I could do against that. I noticed, not for the first time, that, as I read, as the author gains my respect and esteem I tend to give him (or her) the benefit of the doubt. However, people that are always objective throughout their writing probably don't write much so, for the rest, we should remain prudent not to consider everything that is said by any trusted author to be true. The next question that I would expect to ask myself while reading what I wrote is: so, what difference does it make whether an author is trusted (alternatively more trusted) or not (alt. less trusted? Well, for one thing, an author that I trust is one of which I have read many text and it is a little bit less likely that I would be surprised by something he says or write. More importantly, when I hear people talking and I know the particular author is also giving his opinion, I'll give more attention to that author because I trust him. As a corollary, when I have interrogations on topics of which I suspect my author to be interested, I'll first try to find out what his opinion is on the topic. However, it shouldn't mean that I'll be satisfied once I did. As a good computing scientist, I just saw a case where the good behavior to take is ambiguous. If I stress my imagination a lot, I can imagine cases where I trust many authors. What to do? The naive extrapolation is to choose one randomly whenever I need to. It is not very satisfying so I go ahead and look at the next credible solution: to define a more subtle notion of trust for which I can trust author X on topic Z more than I trust author Y on topic Z. If I take one topic at a time for my investigations, this should be fine-grained enough. As a final note, I am not stating that this is what I usually do. It is more like the exposition of a judgment error I do more often than I would like to and a possible solution that I would like to adopt. Simon Hudon Zürich August 19th 2009

Friday, August 14, 2009

Pondering about Reasoning Errors

This note is mostly about teaching and, in general, communicating with other human beings. I have thought about writing it for a while but I was afraid not to have enough material. I'm writing it now because of new observations and I don't care too much about the length, today. In logic, we have the two important notions of soundness and of completeness. In short, a logical system is sound if you can only use it to prove statements that are true (but maybe not all of them) and complete if you can prove all statements that are true (but maybe also some false statements). I mention them because they appear more and more relevant to the way I choose to explain or with which I choose to help people. In such cases, it is necessary to make assumptions in order to explain or skip notions. Two kinds of errors are of interest for me here: either I assume that the other person does not know something and choose to explain it while he or she already know about it or I assume that he or she does and skip it while he or she does not know about it. In the first case, the reaction can be to be insulted because the attitude seems patronizing because the notion seems obvious. In the second case, the other person can miss a notion and be too afraid to appear stupid to ask about it. While I was an intern at A2M (a game developer in Montreal), my supervisor, which I regard with high respect, taught me that it is desirable to make communications as simple and concise as possible and to trust that the other person (in this situation an engineer or a scientist) will not be shy to ask about the missing parts. During the last hour, I've been thinking about this post while doing my groceries and I realized that there are a handful of people that I trust enough to be very straightforward in my communications because I've been talking to them for a long enough period to see that they are active while listening. For the others, it does not mean they are any less. It just means that I don't know if they will ask questions and, from time to time, I don't want to risk them misunderstanding me. In no case is this a sign that I mistrust someone's intelligence because I noticed recently that I was too explicit even with some people which I have in high esteem. This is pretty short but it's all I could summon before my stomach started threatening me. Simon August 14th 2009 Zürich