Viewing profile — housecarpenter

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, a…

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 …

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 g…

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 satisfac…

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 …

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 enti…

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, o…

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 ca…

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 uni…

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)? O…

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 woul…

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…

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 "n…

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 aesth…

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…

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 te…

> 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 countabl…

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…

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 struct…

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 formaliz…