housecarpenter

เดือนที่แล้วdiscuss

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 how our mind works, it seems premature to rule out this possibility. Rather, I would say that ruling it out betrays an assumption that we understand how the mind works enough that we can say that it is definitely not replicable by a machine, and that assumption seems unjustified.

housecarpenter

2 เดือนที่ผ่านมาdiscuss

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 materialists to believe that AI will never be conscious, and AI being perceived as conscious would be problematic for companies that want to provide AI as a product.

housecarpenter

2 เดือนที่ผ่านมาdiscuss

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 presented in isolation. Words like "teal", "cyan", etc. aren't really part of my normal vocabulary and to the extent that they are, I would think of them as subsets of blue or green, not disjoint sets.

I think the test can be fairly criticised on the basis that it is assuming everyone's psychological colour space has a discrete boundary between blue and green, which clearly isn't the case for some people (like you), but it is for others (like me).

housecarpenter

2 เดือนที่ผ่านมาdiscuss

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 community. I believe mathematicians generally consider proving something to the mathematical community the "hard part", while making it fully formal is just a kind of tedious bookkeeping thing.

housecarpenter

5 เดือนที่ผ่านมาdiscuss

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 writing it and testing it. Like 90% verified already. I see code review as just one small stage in the verification process, not the whole of it.

The way I approach it, it's really more about checking for failures, rather than verifying success. Like a smoke test. I scan over the code and if anything stands out to me as wrong, I point it out. I don't expect to catch everything that's wrong, and indeed I don't (as demonstrated by the fact that other members of the team will review the code and find issues I didn't notice). When the code has failed review, that means there's definitely an issue, but when the code has passed review, my confidence that there are no issues is still basically the same as it was before, only a little bit higher. Maybe I'm doing it wrong, I don't know.

If I had to fully verify that the code was correct when reviewing, applying the same level of scrutiny that I apply to my own code when I'm writing, I feel like I'd spend much longer on it---a similar time to what I'd spend writing on it.

Now with LLM coding, I guess opinions will differ as to how far one needs to fully verify LLM-generated code. If you see LLMs as stochastic parrots without any "real" intelligence, you'll probably have no trust in them and you'll see the code generated by the LLM as being 0% verified, and so as the user of the LLM you then have to do a "review" which is really going from 0% to 100%, not 90% to 100% and so is a much more challenging task. On the other hand, if you see LLMs as genuine intelligences you'd expect that LLMs are verifying the code to some extent as they write it, since after all it's pretty dumb to write a bunch of code for somebody without checking that it works. So in that case, you might see the LLM-generated code as 90% verified already, just as if it was generated by a trusted teammate, and then you can just do your normal review process.

housecarpenter

5 เดือนที่ผ่านมาdiscuss

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.

housecarpenter

7 เดือนที่ผ่านมาdiscuss

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 "devastation of the habitat surrounding Hyperion" caused by visitors. Its base was trampled by the overuse and as a result ferns no longer grow around the tree.[13]

Measures to protect the Hyperion tree were officially implemented in 2022 when the National Park Service (NPS) closed public access to its location in Redwood National Park.[14][15] Anyone who gets too close could face up to six months in jail and a $5,000 maximum fine.[13][16][17]"

housecarpenter

8 เดือนที่ผ่านมาdiscuss

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 theory. Disputes about foundations of mathematics are more about how easy or elegant it is to do so. (And in fact my impression is they're mostly about subjective, aesthetic considerations of elegance rather than practical considerations of how hard it is to do something in practice, even though the discussion tends to be nominally about the practical side. Quite similar to disputes about programming languages in that respect.)

housecarpenter

9 เดือนที่ผ่านมาdiscuss

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 *, and then you can say a variable is any string consisting of x followed by any number of marks. You can do the same thing with constants, relation symbols and function symbols. This does mean there can only be countably many of each type of symbol but for foundational purposes that's fine since each proof will only mention finitely many variables.

Allowing uncountably many symbols can be more convenient when you apply logic in other ways, e.g. when doing model theory, but from a foundational perspective when you're doing stuff like that you're not using the "base" logic but rather using the formalized version of logic that you can define within the set theory that you defined using the base logic.

housecarpenter

10 เดือนที่ผ่านมาdiscuss

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 dispute the unit square diagonal argument for the existence of sqrt(2) would be to argue that squares themselves are unphysical, since all measurements are imprecise and so we can't be sure that any two physical lengths or angles are exactly the same.

But actually, this argument can also be applied to 1 and other discrete quantities. Sure, if I choose the length of some specific ruler as my unit length, then I can be sure that ruler has length 1. But if I look at any other object in the world, I can never say that other object has length exactly 1, due to the imprecision of measurements. Which makes this concept of "length exactly 1" rather limited in usefulness---in that sense, it would be fair to say the exact value of 1 doesn't exist.

Overall I think 1, and the other integers, and even rational numbers via the argument of AIPendant about egg cartons, are straightforwardly physically real as measurements of discrete quantities, but for measurements of continuous quantities I think the argument about the unit square diagonal works to show that rational numbers are no more and no less physically real than sqrt(2).

housecarpenter

ปีที่แล้วdiscuss

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 does.

housecarpenter

3 ปีที่แล้วdiscuss

Should it really though? Maybe pedagogy is just hard and we can't expect constant progress.

housecarpenter

3 ปีที่แล้วdiscuss

Isn't this a fairly simple way of doing this? That said, it is a bit non-obvious if you haven't seen it before.

    select earliest_joiner.* from employees as earliest
    left join employees as earlier on
      earlier.role = earliest.role
      and earlier.join_date < earliest.join_date
    where earlier.id is null
    order by earliest.join_date

comments