Although I do not think that anything can propagate at the speed greater than the speed of light (in vacuum), I, too, am not a big believer in gravitational waves: while a wave must be described, from the quantum-mechanical standpoint, as a particle (graviton), I do not see how the geometrical notion of a curvature of space-time can be expressed in terms of one.
Equally naive seem to me attempts to explain the inertial mass using a misterious Higgs boson. The inertial mass is equal to the gravitational mass, so the Higgs particle would have to react to the space-time curvature in a perfectly co-ordinated way, which makes me doubt in its existence. The phenomenon of inertia seems to be more likely a purely relativistic effect.
It is a good thing IMO. You can have multiple virtual sessions / multiple virtual terminals within, say, one SSH session; plus, the ability to detach from the session and re-attach to it later--possibly from other terminal--is very nice.
Reading this (using firefox) on sw-10.2/fluxbox; sweet. Maybe I just hate desktops, then.
After having used/tried several distros (including infamous Ubuntu; liked LFS, Gentoo and Debian), I keep coming back to Slackware - has always worked for me best. It just feels simple and reliable; I am not sure why though (I am not a Unix geek). Somehow it gives me this feeling of freedom I do not have when I use other distros (including Gentoo): this is the only distro (other than LFS) where I do not feel guilty when I happen to compile some app from the stock source tarball instead of using the distro-specific package.
Maybe, I just like Unix in its more or less basic form, as opposed to behemoths (OS X, Ubuntu, Suse) people build on top of it. Slackware, I think, is as basic as it gets, and that's what makes it perfect.
using the printer's CPU engine to calculate the digits!
I do remember them saying that in those days printers' CPUs were more powerful than the computers': PCs were too slow at interpreting PostScript. Too bad that these days' printers aren't that brainy any more: they all rely on drivers...
To this geek, maybe. But it is really idiotic anyway. Example: one of the big advantages of ebooks is being able to search the text. You'd need a mechanical page flipper to browse the search results, then.
HDTV is badly needed, now that everybody loves Raymond!
One of the greatest inventions of the 20-th century, with the huge potential for educating the public, has been used for making said public misinformed, bored, lazy and stupid - in other words, the ideal material for ever-expanding government and commercial control.
90% of TV/radio programs are designed as instruments of brain-washing and/or explicit or implicit commercial advertisement. HDTV will definitely make such programs more effective.
There is a difference: Java is portable, C# is Windows-only (and don't get me started on non-Microsoft, non-Windows implementations of it). In my view, this difference is so important, that it seems foolish to even compare Java and C#: (almost) same syntax, different APIs, different platforms...
It surprises me that hosted computing services are not as wide-spread as they could be. The IT infrastructure of a typical small or midsize business can and should be outsourced: broadband is not a problem these days, and, I assume, Linux would play better (than Windows) in an environment based on the use of thin clients that are not expensive to set up or maintain.
I was talking about a different thing - that there is a similarity between proofs and algorithms; since it is usually not a big problem to translate a well-understood algorithm into a ("formal") program, I expect a similar process of formalizing a proof to be not much more difficult.
When "formalizing" an algorithm, you would normally use a high-level programming language rather than a machine code, and you would use libraries for, say, processing of text objects; the resulting program is usually not very big. Why would not you do something similar when formalizing a proof?
There have been some efforts in that direction; see, for example, metamath.
I do not suggest publishing only formalized proofs, or teaching mathemetics using formalized proofs. But if you have a "library" of formalized theorems (similar to having a library of subroutines), then it should be possible to translate your proof to a formal text that is not long, boring or unclear. And, in the end, you could add your new proof to the library!
I believe that in time it will become the common practice, to publish both an "informal" and a formal proof.
The realization of the striking similarity between proofs and algorithms will eventually make the complete formalization a natural part of the mathematical culture.
This all has purely theoretical interest. We trust computers doing much more important things than proving theorems. You are arguing with the obvious. Of course computers are more efficient than humans in (formally) validating proofs, and of course we can and should trust (well-tested) programs.
it is hard to write a program which can spot contradictions in any argument written in natural English
Mathematical language is much more formalized than "natural English" is. A proof is analogous to (a description of) an algorithm, and it shouldn't be more difficult to validate a proof using a computer than it is to convert an algorithm to a program that can be actually run on a computer.
It has been known for a century that mathematics can be formalized, and so it is remains a mystery why the question of automatic proof validation still generates a controversy.
I was told horror stories of the Soviet Union, about how to go between republics I'd have to show my papers at a checkpoint so they could track who I was and where I was going.
Those were lies. There were (and I am sure still are) checkpoints around so-called "closed zones" - large naval bases, borders, even some small cities where secret institutions were located, etc., but never around entire republics.
UNIX proper (the API, the shell, the commands) is only 1% of "Linux" these days. The rest is provided by infrastructures of KDE and Gnome.
Which is good, because UNIX, as much respected and constantly hyped in the community as it is, must go, because it is obsolete (and has been for quite a while). Creating BeOS was a move in the right direction, but BeOS is only a desktop OS; there is a need in a modern, efficient and well-organized server infrastructure as well. Longhorn, with its object-orientation and a database-like file system is Microsoft's answer to that need; OSS community has to have an answer of its own; and UNIX is not an answer.
Shouldn't WMs just, well, manage windows? Why do they have to be in control of rendering text?
Besides, why are differences between WMs such a big deal? If a WM is configurable and "themable" - isn't this all that anybody would ever need?
IMO, a WM should be given *one* task (that of window management) and be able to co-operate with other management services (or components), such as a theme manager, a font renderer etc.
The idea that the reality can be "fully" described is reductionist by itself and thus cannot be used as an argument in support of reductionism.
That the above idea is wrong becomes obvious from the fact that one would not be able to explain, say, a perfectly real historical event based on particle physics: human society can only be understood using special models that have nothing to do with physics.
If you are religious, you can only believe that you are a scientist.
Although I do not think that anything can propagate at the speed greater than the speed of light (in vacuum), I, too, am not a big believer in gravitational waves: while a wave must be described, from the quantum-mechanical standpoint, as a particle (graviton), I do not see how the geometrical notion of a curvature of space-time can be expressed in terms of one.
Equally naive seem to me attempts to explain the inertial mass using a misterious Higgs boson. The inertial mass is equal to the gravitational mass, so the Higgs particle would have to react to the space-time curvature in a perfectly co-ordinated way, which makes me doubt in its existence. The phenomenon of inertia seems to be more likely a purely relativistic effect.
It is a good thing IMO. You can have multiple virtual sessions / multiple virtual terminals within, say, one SSH session; plus, the ability to detach from the session and re-attach to it later--possibly from other terminal--is very nice.
Reading this (using firefox) on sw-10.2/fluxbox; sweet. Maybe I just hate desktops, then.
After having used/tried several distros (including infamous Ubuntu; liked LFS, Gentoo and Debian), I keep coming back to Slackware - has always worked for me best. It just feels simple and reliable; I am not sure why though (I am not a Unix geek). Somehow it gives me this feeling of freedom I do not have when I use other distros (including Gentoo): this is the only distro (other than LFS) where I do not feel guilty when I happen to compile some app from the stock source tarball instead of using the distro-specific package.
Maybe, I just like Unix in its more or less basic form, as opposed to behemoths (OS X, Ubuntu, Suse) people build on top of it. Slackware, I think, is as basic as it gets, and that's what makes it perfect.
Lackware - not a bad name for a new minimalist distribution.
I do remember them saying that in those days printers' CPUs were more powerful than the computers': PCs were too slow at interpreting PostScript. Too bad that these days' printers aren't that brainy any more: they all rely on drivers...
To this geek, maybe. But it is really idiotic anyway. Example: one of the big advantages of ebooks is being able to search the text. You'd need a mechanical page flipper to browse the search results, then.
I could not think of anything more stupid.
Ah, this eternalle questionne of Goodle vs. Eville...
HDTV is badly needed, now that everybody loves Raymond!
One of the greatest inventions of the 20-th century, with the huge potential for educating the public, has been used for making said public misinformed, bored, lazy and stupid - in other words, the ideal material for ever-expanding government and commercial control.
90% of TV/radio programs are designed as instruments of brain-washing and/or explicit or implicit commercial advertisement. HDTV will definitely make such programs more effective.
... havoc wreaks YOU!
There is a difference: Java is portable, C# is Windows-only (and don't get me started on non-Microsoft, non-Windows implementations of it). In my view, this difference is so important, that it seems foolish to even compare Java and C#: (almost) same syntax, different APIs, different platforms...
Bash under Cygwin. Functional and beautiful!
And being the first in space, too, was cheap.
It surprises me that hosted computing services are not as wide-spread as they could be. The IT infrastructure of a typical small or midsize business can and should be outsourced: broadband is not a problem these days, and, I assume, Linux would play better (than Windows) in an environment based on the use of thin clients that are not expensive to set up or maintain.
I was talking about a different thing - that there is a similarity between proofs and algorithms; since it is usually not a big problem to translate a well-understood algorithm into a ("formal") program, I expect a similar process of formalizing a proof to be not much more difficult.
When "formalizing" an algorithm, you would normally use a high-level programming language rather than a machine code, and you would use libraries for, say, processing of text objects; the resulting program is usually not very big. Why would not you do something similar when formalizing a proof?
There have been some efforts in that direction; see, for example, metamath.
I do not suggest publishing only formalized proofs, or teaching mathemetics using formalized proofs. But if you have a "library" of formalized theorems (similar to having a library of subroutines), then it should be possible to translate your proof to a formal text that is not long, boring or unclear. And, in the end, you could add your new proof to the library!
I believe that in time it will become the common practice, to publish both an "informal" and a formal proof.
The realization of the striking similarity between proofs and algorithms will eventually make the complete formalization a natural part of the mathematical culture.
This all has purely theoretical interest. We trust computers doing much more important things than proving theorems. You are arguing with the obvious. Of course computers are more efficient than humans in (formally) validating proofs, and of course we can and should trust (well-tested) programs.
Mathematical language is much more formalized than "natural English" is. A proof is analogous to (a description of) an algorithm, and it shouldn't be more difficult to validate a proof using a computer than it is to convert an algorithm to a program that can be actually run on a computer.
It has been known for a century that mathematics can be formalized, and so it is remains a mystery why the question of automatic proof validation still generates a controversy.
Those were lies. There were (and I am sure still are) checkpoints around so-called "closed zones" - large naval bases, borders, even some small cities where secret institutions were located, etc., but never around entire republics.
True Linux hackers eat their dog's food.
UNIX proper (the API, the shell, the commands) is only 1% of "Linux" these days. The rest is provided by infrastructures of KDE and Gnome.
Which is good, because UNIX, as much respected and constantly hyped in the community as it is, must go, because it is obsolete (and has been for quite a while). Creating BeOS was a move in the right direction, but BeOS is only a desktop OS; there is a need in a modern, efficient and well-organized server infrastructure as well. Longhorn, with its object-orientation and a database-like file system is Microsoft's answer to that need; OSS community has to have an answer of its own; and UNIX is not an answer.
Shouldn't WMs just, well, manage windows? Why do they have to be in control of rendering text?
Besides, why are differences between WMs such a big deal? If a WM is configurable and "themable" - isn't this all that anybody would ever need?
IMO, a WM should be given *one* task (that of window management) and be able to co-operate with other management services (or components), such as a theme manager, a font renderer etc.
> fully describe reality
The idea that the reality can be "fully" described is reductionist by itself and thus cannot be used as an argument in support of reductionism.
That the above idea is wrong becomes obvious from the fact that one would not be able to explain, say, a perfectly real historical event based on particle physics: human society can only be understood using special models that have nothing to do with physics.
Reductionism is nothing but a common mistake. There is a large number of obvious arguments against it.
The behavior of a fluid can be modeled without bringing in the notion of a quark.
Mathematically, the axioms on which one can build hydrodynamics are not required to contain the definition of a particle.
In programming, an analogy would be the fact that an interface cannot be reduced to a specific implementation.