Long time no see. I have posted my latest OOPSLA submission.
At long last I feel like I am making progress again. I have been stuck on this problem for the last 9 months. The worst part is that people kept asking me “What are you working on?”, and I would say, “Well, I am trying to figure out how to do conditionals, and I am really stuck”. This produced funny looks. I mean, what kind of moron can’t figure out how to do conditionals? What could be hard about that? Well, I think I have finally figured out how to do conditionals.
The next paper will probably be about how to do loops. But first I need to do some honest coding…
Great! I look forward to reading it, once I finish up my own FSE submission.
Very cool! I skimmed the first couple of pages, said “I gotta see the pictures!”, and I could immediately get the gist of things from the first few diagrams. This is VERY promising — can’t wait to see where it goes!
At first glance it looks very interesting. However, could you make an electronic version of the document available? I don’t like to print papers out so the figure placement at the end doesn’t work for me, and I think you could probably also inline a movie in the PDF document to make the paper more clear.
By the way, I’ve just finished my ONWARD submission. Its related to subtext, if you are interested you can find it here:
http://lamp.epfl.ch/~mcdirmid/mcdirmid07live.pdf
Correction?
On Page 6 (Section 4) when describing Figure 14. #2 has the line “For example the first input to the ‘+’ function…”. I think this is actually a ‘*’ multiplication function, according to the Java code. I actually found the function box to the right of the ‘effectiveness’ and the one in the magical column below “1 – target.magic” to be unclear – should they not have some kind of description as to the kind of math they perform?
Ahhh, on page 16, i see that figure 15 has the ‘*’ in the boxes that i complain about in the previous entry (for figure 14).
I like this approach a lot. Obviously there are plenty of open questions, but you’re quite frank about that, and I think it’s very promising. I do have a few comments:
1. A tiny nitpick: the Third Patriarch’s name should probably be either Sengcan (Pinyin) or Seng-ts’an (Wade-Giles). You could probably get away with Sengtsan, but Sengstan is just wrong. 🙂
[Right, typo. His name seems to be traditionally translated as Sengtsan.]
2. I’m not completely sure, but I feel like the Java code in Figure 7 might actually be incorrect, or at least wrong wrt Figure 6. If a, b, and c are all false, Figure 6 sets x to 3, while Figure 7 sets x to 2. It’s an interesting error because it only serves to make your point stronger! Apparently, even “intense concentration” isn’t always enough. Also, it’s a little odd stylistically to see the bitwise operators used for booleans in Java code. In fact, I was a little surprised it works.
[OMG! You’re right. Fixed on my website. Unfortunately the correct solution makes the problem look easier, at least in retrospect. Ironic.]
[Duh! Fixed it again. Embarrassing, but it does make my point rather dramatically.]
[BTW, those aren’t bitwise operators – they are the REAL boolean operators in Java, not the short-circuit ones we all use to bum a little performance.]
3. It would be nice to see an example of laminar browsing working on a column other than the rightmost one. I’m not sure I can imagine how this would work, visually. It appears that this might be happening in Figure 21, but there’s not enough context to be sure.
[Yes, Fig 21 is an example. Since every function is on its own row, you can expand rightward from any column without ambiguity. Will have to see how it plays out when implemented.]
4. Given the lack of a conventional compile-/run-time distinction in Subtext, I’d consider using different terms to talk about predicate and assertion checking. It might be better to use static/dynamic, which I think captures the distinction you’re really making (static properties being verifiable based only on the structure of the system, while dynamic properties depend on actual values). More generally, I didn’t find the stuff about static analysis completely convincing. I’ll be curious to see how much of the predicate/assertion checking can actually be done statically.
[Yes, that might be better. It seemed to me that compile-time/run-time was the least surprising, though not the most accurate.]
Finally, a question: it appears from Section 7 (Decidability) that the partitioning requires predicates to be formally axiomatized. But many programs have predicates that relate in non-obvious ways… Will the user be able to add axioms to the system? For example, I might have complicated conditional logic involving a bunch of authentication predicates like isUserAuthenticated(), isUserRegistered(), isUserGuest(), etc… While these are not necessarily mutually exclusive (if they were, we could just use an enumeration and get our axioms for free), it’s often the case that only certain combinations of predicates are possible. In my experience, this is some of the worst conditional logic, since understanding the impact of a change requires understanding the interacting semantics of the various predicates. I’d really like to think that this approach can help in cases like this, but it’s not obvious to me that it will. If this direction is interesting to you, I’d be glad to discuss it further.
[Excellent observation. I want to handle this by allowing the programmer to make assertions that state logical relationships between predicates, essentially writing your own axioms, but also checking them at run-time. Assertions will need to be generalized to handle this. Let me get back to you on this when I have gotten deeper into the implementation.]
All in all, I really enjoyed this paper and I really look forward to seeing an implementation. Thanks!
[Thanks for the penetrating comments. Can I hire you to review my next paper? — Jonathan]
FYI
Lambda the Ultimate has an entry on the OOPSLA submission:
http://lambda-the-ultimate.org/node/2148
to quote(ish) HHGttG/?R@tEotU, “bloody hell, Broom-fon-del, now that’s what i call thinking. how come we never think of things like that? … dunno – guess our minds must be too highly trained.”
revisiting the basics like this is just a warm fuzzy joy to see. please keep at it.
Wonderful stuff (from someone who is normally a skeptic in these matters). See my fuller comments over on LtU.
Matt Hellige\’s comments on partitioning are quite important. In general, this is nastily undecidable. However, as most people doing static analysis of real programs have discovered (myself included), most programs fall into classes where the partitioning problem is decidable. Actually, if a program has that complex a partitioning problem, one wonders if that\’s really what the programmer meant!
Anyways, there is lots of people with 20 years of experience using tabular notation for specification of real-time safety-critical systems who would back you up on the usefulness of this notation. You already cite C. Heitmeyer\’s work, you can also look at some of Alan Wassyng\’s (Alan was an industry consultant on real-time safety-critical systems for 20 years, working on proving specifications correct, mostly via tabular notations).
[Thanks for the very positive comments. You are quite right that I should look more deeply into the prior work on tabular specification languages. I am choosing a somewhat different notation, but much of the theory and analysis techniques may be applicable.
You make a good point on LtU about Dijkstra\’s guarded commands. I like your perspective that Dijkstra uses overlapping to express non-determinism, while I am interpreting it as erroneous ambiguity. Interesting contrast.
–Jonathan]
I’ve left some comments on LtU that are more indepth though also more unintelligble. Anyway, I’ve butchered your diagrams in order to make a suggestion:
http://putstuff.putfile.com/61948/258564/3
Sorry for the crappy file host…
Anyway, I know that you suggested that something like this might be possible – factoring some of it into a seperate function, however, I think something like anonymous functions (lambdas) might be applicable here. So, I’ve doodled up some gui interactions and results in that file (I had to trace to vector, so it’s pretty bad. Hopefully by the end of SoC inkscape will have pdf import…)
I realize that this breaks a ton of the purity of your idea – and messes up the parameter thing too, however, I think this and things like it are necessary for practicality sake, as syntax sugar. (Parameter order etc should be dealt with some other way anyway).
Hmm, I forgot to show re-merging the anonymous function into the original table, however, that should be possible too – if the user wants to add more interesting logic to it, using the space that was empty before.
Anyway, thanks for working on this stuff. It’ll probably be very influential in my future visual language designs (I’ve been thinking about them for a while; can I use this stuff?). It happens to coincide very well with some other ideas I’ve had.
[Michael – thanks for the comments and suggestions. I envision functional abstraction working by pushing code into a nested box, rather than pulling it outside as your sketch suggests. But I need to experiment with it. I encourage you to work further on your ideas, and feel free to incorporate any of mine. My measure of success is to have ideas good enough to be worth stealing 🙂 . – Jonathan]
I really likes your innovation! It shows that CS dont stands for “Compiler and Syntax” (or “Cryptic Symbols”).
We needs more innovations and logic and less CSI-oriented programming (Compiler, Syntax, Implementation).
The “Crime Scene Investigation” starts when you have changed the implementation in a way that gives you an error from the tests.
I do not understand why, but Google could not find “CSI-oriented programming”. Is it another innovation?