Why is asking 'can machines think?' assuming our thinking could be modeled as a machine? It's raising the possibility that our thinking could be modeled as a machine. Given that, as you acknowledge, we don't have a clue…
Why would it serve the interests of AI companies to promote materialism? It seems to me that idealism would be more in the interest of AI companies to promote, since my impression is idealists are more likely than…
I don't think that's necessarily the case. I understand that there's a continuum in reality, but psychologically, I still tend to perceive each shade as discretely either blue or green, especially when the shade is…
Isabelle/HOL haven't been solving open problems, as far as I'm aware. They've been used for making fully-formal proofs of problems that were already considered proved to a satisfactory level by the mathematical…
The reason I don't spend the majority of my time in code review is that when I'm reviewing my teammates' code I trust that the code has already been substantially verified already by that teammate in the process of…
It's true that onomatopoeia isn't always a word, but in the particular case of "aah", I think that particular choice of letters is conventionalized enough that it is a word.
From Wikipedia: "The exact location of Hyperion is nominally secret but is available via internet search.[12] However, in July 2022, the Redwood Park superintendent closed the entire area around the tree, citing…
My impression (as a dilettante programmer without relevant credentials) is that there isn't really any question about whether mathematical structures can be rooted in set theory, or can be expressed as extensions of set…
Defining first-order logic doesn't really require set theory, but it does require some conception of natural numbers. Instead of saying there's an infinite set of variables, you can have a single symbol x and a mark *,…
My first thought on reading your comment was to disagree and say no, we can have the exact value of 1, because we can choose our system of units and so we can make the square a unit square by fiat. A better way to…
Consider the identity function f, which just takes an argument and returns it unchanged, and has the polymorphic type a -> a, where a is a type variable. What's the type of f(f)? Obviously, since f(f) = f it should be a…
It would surprise me if most rationalists didn't know who Jaynes was. I first heard of him via rationalists. The Sequences talk about him in adulatory tones. I think Yudkowsky would acknowledge him as one of his…
What do you find surprising---the fact that it doesn't come out red, or the fact that people are confused by this behaviour?
At least in my country (the UK), people generally do not learn abstract algebra in high school. That's a university-level topic. I think there is a definite "step up" in complexity between the structures of abstract…
It is a particular sense of "nondeterminism", but it's not specific to functional programming, I think it's the usual one theoretical CS as a whole. It's the same sense in which "nondeterminism" is used in P vs NP, for…
As a non-arachnophobe, I don't find spiders of any kind to be cute. But I also don't find anything about their appearance or behaviour to be unpleasant or scary. They're just aesthetically unremarkable. Similar to, say,…
As somebody with autism, one thing I'd say from my experience (I don't know how many people will agree) is that interviewing has felt like a much more severe stress test of my soft skills than anything I've had to do…
I think the author made a typo, and they actually meant to refer to 2.92, not 2.29. The table preceding the part mentioning 2.29 only includes 2.92. And 2.29 doesn't include the text "This is not easy!”, whereas 2.92…
> it is absolutely completely impossible to randomly put a dot down on a number line and have it be pi It's not impossible, it just has zero probability of occurring.
An spoken English sentence is a finite string of phonemes. The set of allowable phonemes is finite. Given a finite set X, the set of all finite strings of elements of X is countable. (The latter statement holds because…
What do you mean by "the use of the Least Upper Bound"?
Can you elaborate on why?
Technically, `a :: Num` would be declaring, or defining that `a` is of type `Num`. After you see `a :: Num`, you can assume from then on as you're reading the program that `a` has type `Num`; if something is…
As I understand it, the main advantage of having separate CUSTOMER and ORDER tables rather than just have a field on CUSTOMER which is a list of order IDs is that the latter structure makes it easy for someone querying…
You can absolutely formalize proofs using diagonalization arguments on a computer in just the same way you would formalize any other proof. For example here's the Metamath formalization of Cantor's argument that a set…
Why is asking 'can machines think?' assuming our thinking could be modeled as a machine? It's raising the possibility that our thinking could be modeled as a machine. Given that, as you acknowledge, we don't have a clue…
Why would it serve the interests of AI companies to promote materialism? It seems to me that idealism would be more in the interest of AI companies to promote, since my impression is idealists are more likely than…
I don't think that's necessarily the case. I understand that there's a continuum in reality, but psychologically, I still tend to perceive each shade as discretely either blue or green, especially when the shade is…
Isabelle/HOL haven't been solving open problems, as far as I'm aware. They've been used for making fully-formal proofs of problems that were already considered proved to a satisfactory level by the mathematical…
The reason I don't spend the majority of my time in code review is that when I'm reviewing my teammates' code I trust that the code has already been substantially verified already by that teammate in the process of…
It's true that onomatopoeia isn't always a word, but in the particular case of "aah", I think that particular choice of letters is conventionalized enough that it is a word.
From Wikipedia: "The exact location of Hyperion is nominally secret but is available via internet search.[12] However, in July 2022, the Redwood Park superintendent closed the entire area around the tree, citing…
My impression (as a dilettante programmer without relevant credentials) is that there isn't really any question about whether mathematical structures can be rooted in set theory, or can be expressed as extensions of set…
Defining first-order logic doesn't really require set theory, but it does require some conception of natural numbers. Instead of saying there's an infinite set of variables, you can have a single symbol x and a mark *,…
My first thought on reading your comment was to disagree and say no, we can have the exact value of 1, because we can choose our system of units and so we can make the square a unit square by fiat. A better way to…
Consider the identity function f, which just takes an argument and returns it unchanged, and has the polymorphic type a -> a, where a is a type variable. What's the type of f(f)? Obviously, since f(f) = f it should be a…
It would surprise me if most rationalists didn't know who Jaynes was. I first heard of him via rationalists. The Sequences talk about him in adulatory tones. I think Yudkowsky would acknowledge him as one of his…
What do you find surprising---the fact that it doesn't come out red, or the fact that people are confused by this behaviour?
At least in my country (the UK), people generally do not learn abstract algebra in high school. That's a university-level topic. I think there is a definite "step up" in complexity between the structures of abstract…
It is a particular sense of "nondeterminism", but it's not specific to functional programming, I think it's the usual one theoretical CS as a whole. It's the same sense in which "nondeterminism" is used in P vs NP, for…
As a non-arachnophobe, I don't find spiders of any kind to be cute. But I also don't find anything about their appearance or behaviour to be unpleasant or scary. They're just aesthetically unremarkable. Similar to, say,…
As somebody with autism, one thing I'd say from my experience (I don't know how many people will agree) is that interviewing has felt like a much more severe stress test of my soft skills than anything I've had to do…
I think the author made a typo, and they actually meant to refer to 2.92, not 2.29. The table preceding the part mentioning 2.29 only includes 2.92. And 2.29 doesn't include the text "This is not easy!”, whereas 2.92…
> it is absolutely completely impossible to randomly put a dot down on a number line and have it be pi It's not impossible, it just has zero probability of occurring.
An spoken English sentence is a finite string of phonemes. The set of allowable phonemes is finite. Given a finite set X, the set of all finite strings of elements of X is countable. (The latter statement holds because…
What do you mean by "the use of the Least Upper Bound"?
Can you elaborate on why?
Technically, `a :: Num` would be declaring, or defining that `a` is of type `Num`. After you see `a :: Num`, you can assume from then on as you're reading the program that `a` has type `Num`; if something is…
As I understand it, the main advantage of having separate CUSTOMER and ORDER tables rather than just have a field on CUSTOMER which is a list of order IDs is that the latter structure makes it easy for someone querying…
You can absolutely formalize proofs using diagonalization arguments on a computer in just the same way you would formalize any other proof. For example here's the Metamath formalization of Cantor's argument that a set…