Slashdot Mirror

I use the desktop wall, but the cube doesn't have to float windows.

Both of those tools use the GPU, nothing of which I am aware but Metisse is an actual 3D desktop for X.

There's no point in waving your hands around in midair unless you have STUFF in midair, like they did in Minority Report or Johnny Mnemonic. We need holographic displays or lightweight, high-resolution head-mounted displays before there will be any point whatsoever in using anything other than ye olde keyboard and mouse (or trackball). The combination of a high-res eyetap, data gloves or hand tracking, and Metisse would be a working starting point if Metisse-transformed windows could be composited etc.

Mettise uses pie menus, though that's probably the least of its innovations.

(Or more generally see the main Verisoft page. When posting on C verification perhaps one also should mention Caduceus)

A 7 stone handicap is still HUGE. I've beaten a professional (Kano 7d) with that handicap. Sure, but it certainly puts to rest your boast: There isn't a go program running on anything that I can't give a 9 stone handicap to and crush almost without thinking - and I'm only 2k. The day a computer beats a pro seems to be far in the distant future. So, not only has a computer already beaten a pro, but the pro was actually one of the top at the game, having won a major tournament. Care to wager about beating that program giving it a 9-stone handi yourself? Come on, you said that you could crush any go program running "almost without thinking" with that handicap. Go may be complex, and the complexities of strategic thinking are really hard (including even the most basic "big" vs. "vital" concepts), but clearly Go computer programs have gotten way beyond where you thought they were. At this point, it seems like there are at least some programs that outpace your expectations. It is entirely conceivable that Go programs could be good enough in a mid term time frame that they give stones to all but the Dans & pros. Regards.

I downloaded the latest publicly available version of MoGo (release 3) and I have to say I was fairly impressed. The program beat me a couple of times at a 9 stone handicap but now I can beat it. Here is the first game I played. This is the first game I won. The trouble is that go-playing programs make a systemic pattern of mistakes that's readily apparent after playing a few times. Mogo seems to have a much better "concept" of eyeshape than other programs I've played. Its main overall strategy seems to be to play in a different part of the board (tenuki) when it can't read the local situation, which is actually a valid strategy (used by human players) so long as it doesn't neglect critical situations.

I was really impressed with the way the program uses your time to analyse the position (--pondering flag) and that it resigns when it sees the game as hopeless, although it did resign a game that it had won. The program also keeps track of the time and adjusts its analysis correspondingly, which I've never seen a program do before. Still, there is a loooong way to go.

FYI, the program I downloaded is the 64-bit precompiled linux version running on a 2.2 GHz dual-core AMD under the current Gentoo release, using the GoGui front end. The program was invoked with the options --19 --totalTime 600 --nbThreads 2 --pondering 1

While MFoG is certainly respectable, there are go AIs that work native under Linux you may want to look into, such as the open-source gnugo and the incredibly strong mogo.

The technique used to make MFoG 12 so strong (Monte Carlo Tree Search) was first popularized for go AI by Mogo, and last I checked Mogo was still stronger than MFoG. Check it out.

I don't know the specifics of handicapping in go...

With Mogo taking a nine-stone handicap, our Korean 8-dan professional should have been favored to win by mere slaughter, instead of nuclear annihilation. Instead, the pro lost. This result is astonishing.

Anyone who has ever played Mogo (the program is freely available at http://www.lri.fr/~gelly/MoGo_Download.htm ) will instantly recognize Mogo's 1.5 point advantage as typical of the program's usual conservative style in the endgame. It always plays to win by the least amount necessary and takes no chances.

For anyone interested, MoGo was the Phd thesis of Sylvain Gelly, and that thesis, which describes mogo, is available here: http://www.lri.fr/~gelly/ As was said before, alpha-beta search is the most common strategy in chess, but my understanding is that it doesn't parallelize very well. Monte Carlo has been around for a long time, but it hasn't ever really succeeded at Go. Gelly's main contribution was to borrow a successful solution to the multi-armed bandit problem, an algorithm called UCB, and apply to the search tree. Initial values are determined through Monte Carlo style search, and then for each branch the algorithm estimates the upper confidence bound on the reward of each move, and preferentially searches the parts of the tree that seem to have good potential. This made it good, but still not quite as good as gnugo, so he used reinforcement learning offline to make a quick pattern-matching style evaluation to aid UCT. There are some other tweaks to improve play style mentioned in the thesis. Anyway, it's worth a look if your interested, and especially if you feel like MoGo has an obvious or boring algorithm.

Indeed. In fact, most of the interesting algorithms come with a proof of correctness and termination. The problem is, traditional programming languages are not expressive enough to specify and prove termination within the language itself. But there are many ways to achieve this : either annotate the program with logical assertions, allowing an external automated demonstration program to *try* to check soundness and completness; or program directly with Coq or PVS. Some links : http://why.lri.fr/ & http://coq.inria.fr/.

I'm a reasonably strong Go player myself (4. dan) and I've studied computational complexity - my gut feeling is that computers will not beat humans at Go in my lifetime even if Moore's law continues to apply. The only possibility is that someone comes up with a completely new approach, a bit like when alpha-beta search was invented for Chess. At the moment the most interesting approach is Monte Carlo methods applied to Go which has so far lead to a gain of at least two stones strength for the current programs. The strongest Monte Carlo based program is currently MoGo by Sylvain Gelly et al. which you can find more information about at http://www.lri.fr/~gelly/MoGo.htm.

This is the 'Monte Carlo' method, yes?

I read some months ago about progress in computer go made this way. I went looking to download one (hoping for a freely available version), but all I found was a small bit that played 9x9 - or maybe it was even smaller.

There's an unspoken visual hint, a scene involving a topdown view of umbrellas in rain on a Tokyo sidewalk in Hikaru no Go, which suggests that when Monte Carlo methods finally apply to Go on the large, 19x19 goban (as they do on the 13x13 board, see MoGo), we resourceful humans will simply sidestep the issue by introducing color to the game. First red, yellow, blue, green, then as computers get uppitier than ever, chartreuse, plum, turquoise, peridot and champagne. It ain't thought until you can change the rules in midstream.

that's not the impression I got from their demonstration videos

I found very useful-looking stuff here, like this.

that's not the impression I got from their demonstration videos

I found very useful-looking stuff here, like this.

Well what is this with "Metisse"?

Heard of Google? ;) Look here

Fvwm-Crystal is really nice, it shows how powerful and flexible Fvwm can be while still being light and fast. But its main drawback is that when something goes wrong, you are screwed unless you know Fvwm very well, and this is not something easy to achieve (for those who don't know Fvwm, just look at the man page.

Also, while we are on the subject of Fvwm, check out Metisse, a nice experimental Fvwm-based OpenGL desktop. I'm not sure if it's still actively maintened though. It would be a nice thing too if they ported it to Xgl.

>>> Could you give an example of what you mean here (e.g. a description of a simple function and why you would always be required to write unit tests)? - do you work? Seriously?

I probably wasn't clear enough, but I meant: what unit tests would you still need to write if your language+tools were powerful enough to determine if your program met its specification at compile-time?

>>> Here is an example: A service code at Bell Canada is a two character description of a program or a service or a piece of rental equipment.

Thanks for the detailed example, but I'm not sure I understand it. Your saying that depending on input to the database in your unit tests, the results of the unit tests will change, making it harder to test statically?

>>> 3. It is necessary to have the unit test check the boundary conditions, and so there is more than one unit test (actually it is the same unit test ran with different data sets on all known boundaries and some cases between the boundaries. The boundaries include empty set, one element in the set per model, an arbitrary number of elements in the set per model, where there is either none, one or an arbitrary number of models.)

>>> 4. There is no way to tell what the models will be, what the packages will be, so there is no way to test for ALL inputs. No amount of time given to an inference engine can ever finish testing a function for an unlimited input size.

This is the perfect thing to tackle with induction, meaning that you can test all inputs in a reasonable amount of time (remember, you're not actually running the program for all results, just proving that it will work for all results). You prove the base case and inductive case and this gives you a proof for all cases.

Of course, it's going to be harder to do this if your inputs/specification are incredibly complex (such as a database). All your functions should be short, as simple as possible and strongly specified to make checking easier. I'm not saying all cases are easy, but the example you gave is fairly exotic.

Here are some small examples of imperative programs that have properties about them proven mathematically (e.g. a sorting algorithm sorts, a square root function finds the square root, a binary search function works):
http://why.lri.fr/examples/

For these examples, there is no need to write any unit tests at all, because you have proven for all possible inputs that it will always work. For instance, the binary search on an array example contains a proof that the algorithm will always return what you are searching for if it is in the tree and that there will never be any buffer overruns statically.

Looking Glass (GPL)

3Dwm (GPL)

Metisse (GPL)

reminds me of metisse if you ask me.
http://insitu.lri.fr/~chapuis/metisse/

I tried the Java demo. I found it a bit slow, and froze for a one second or less each time I dragged something near the border of a window.

So, the idea is interesting, is good, this may be used in future. But it must be fast, faster than the demo.

There is an experimental OpenGL 3D desktop for Linux called Metisse. There is "window folding" in Metisse. Maybe these two could be joined together?

http://insitu.lri.fr/~chapuis/metisse/

I still think the better is to avoid lots of windows on same workspace. I have lots of workspaces in my Linux window manager, and I can keep each one clean. No more than 2 overlapping windows here. Windows users really miss this. I don't know about Mac, but I know Mac users have a lot of good desktop features.

More specifically one would have to compile in libstroke support for the mouse-gestures use metisse for the window-folding effects. After some configuration, one could do many of the very same (or at least nearly the same) things described in the article.

Anyone care to try? :)

i know that for linux there is an experimental interface called Mettisse that allows folding of windows (though fold and drop, i am not sure.) plus a few other things. unfortunately i don't think it's designed at the moment to be used as the primary window manager.

Hello For information this kind of stuff already exists, from long time. I invite you to visit this webpage : http://www.lri.fr/~fedak/XtremWeb/introduction.php 3 Regards

I never get over people saying things like this. It's always seemed like splitting hairs to me. Yes it looks like KDE, just like KDE looks like Windows, Windows looks like GNOME, GNOME looks like Aqua, etc, etc..

All of these popular interfaces use the same metaphors and ideas. For example, they all have some sort of "bar" in one part of the screen that organizes open programs and/or launches programs and/or tells you what time it is and a bunch of other stuff. Call it a "taskbar", a "panel", a "dock", or a "kicker", it's all the same thing.

Interfaces haven't really progressed from these basic ideas since their inception. If you want something that's fundamentally different, look at interfaces like Looking Glass, or Metisse.

For Lisp you could use ACL2. For Java you could use JML , together with Krakatoa, Why (which could also be used to program the solution) and Coq. For all the other languages that appear in the solutions list I think you're on your own.

For Lisp you could use ACL2. For Java you could use JML , together with Krakatoa, Why (which could also be used to program the solution) and Coq. For all the other languages that appear in the solutions list I think you're on your own.

I don't suppose you mean specially optimized compilers like this one by any chance?

The second screen shot about the "Auto Scale mode" looks like a feature that works better than Expose on OS X. The thing I don't like about Expose is having to work with function keys or desktop hot corners in order to activate it. The Auto Scale mode looks like a version of Expose that runs while you are working, without having to resort to function keys or hot spots.

It looks like a feature in which the shrunken windows are visible around the normal size active window, without any overlapping. I presume switching between windows requires you to simply click on a shrunken window, which would resize it to normal and shrink the previously acitve one, kind of similar to Expose.

This also eliminates the need for a Task Bar, and would also have the advantage of actively showing the windows contents, rather than just representing a window with a Task Bar button. OS X can display a minimised window's contents in the dock, but this Auto Scale mode can display minimised window contents in a larger fashion, depending upon the space available on the screen.

I also presumed that Expose was OS X's answer to the Task Bar, because their dock didn't allow you to switch windows as efficiently as the Task Bar. This Auto Scale feature looks like something that is a combination of Expose and the Task Bar, but works better than both. I think this is a really innovative concept for window managers.

CFS and PAST are P2P readonly file systems a la Napster/Gnutella/Freenet. Both had papers in this year's SOSP. Both are based on log(N) P2P overlay routing/lookup substrates.

OceanStore seeks to be a more general (writable) global storage system.

And several P2P conferences have formed and will continue to form.

Some of these projects have been going on for years. So you shouldn't buy the "Academic networking/CS researchers are a bunch of P2P haters" line without a few grains of your favorite seasoning.

I wrote an email to John Carmack about PMesa, which speeds up some OpenGL calculations up to 1.8x on SMP hardware. He said this:

Its not going to help bandwidth limited applications. Applications with lots of evaluators and lighting probably show worthwhile speedups, but basic vertex/texcoord/color drawing probably doesn't get helped at all (unless the basic geometry code is very badly implemented).

John Carmack