doctor_phil

5 dni temudiscuss

I agree, producing a lower bound is possible. It's practically very hard to give a good lower bound though. Many programs do not terminate, so we don't know if they do produce the right output eventually. In practice the best that has been done on Turing machines is that we have now proved which 5-state machines halt and which don't. So proving any lower bounds larger than that is practically impossible.

doctor_phil

5 dni temudiscuss

Overall an interesting blog post, but the author makes this claim several times:

> So you can never close the case on even one candidate, let alone all of them at once, which means the lower bound stays sealed.

Which is simply not true. The specifics depends on what language you use, but let's take Turing machines as an example. Many candidates are easily disproven: ones that halt immediately, ones that have no rule for writing a "1", ones that have no rule for halting and so on. It's impossible to write a program that can handle every possible candidate though.

And if your string is short enough, let's say the string you are investigating is "0011" then you CAN sit down and check all Turing machines of size 4 and lower. This is essentially what the https://bbchallenge.org/ project did.

For Turing machines we have determined if they halt or not for all machines up to 5 states. It is very computationally hard to push this limit further, but we don't know where the theoretical limit is. We have some large upper bound where a Turing machine computes something that we know is independent of ZFC (see Scott Aaronson for more details), but many suspect that the limit is way lower.

doctor_phil

18 dni temudiscuss

Nice, not having bodies on GET has been a pet peeve of mine for a long time. It would be nice to allow bodies on DELETE as well, but that is less of a problem in most cases.

doctor_phil

25 dni temudiscuss

> UBI won't work either because it will lead to [...] extreme levels of invasive control over people's lives and what they can and cannot do

I've never heard this before. I thought UBI would be very freeing and without much control. If it is universal then there needs to be no control of who gets it or not. What am I missing?

doctor_phil

4 miesiące temudiscuss

I also for a second thought this was Rasmus Lerdorf, the creator of PHP. In my head I just have him as Rasmus L-something, so this guy was just a hash collision. :)

doctor_phil

5 miesięcy temudiscuss

Idris is slightly more mainstream I would say, but not wildy so. If you like the Haskell interop then I'd recommend staying with Agda.

Scala 3 is much more mainstream and has path dependent types. I've only used Scala 2, and there the boilerplate for dependent types was frustrating imo, but I've heard its better in 3.

doctor_phil

5 miesięcy temudiscuss

Wow, this is so cool! Very overwhelming with so many interesting things at once. I wish I had a few months with nothing else so I could surround myself with only this. :)

doctor_phil

7 miesięcy temudiscuss

Yes. Metal. No.

You want to read about "conservation of etendue" for a technical explanation. For an easier explanation, look for xkcd's excellent "Fire from Moonlight".

doctor_phil

7 miesięcy temudiscuss

I don't think this blog post reflects so well on this engineering team. Kudos to them to be so transparent about it though. "We had so many flaky tests that depended on 3rd parties that broke pipelines that we decided on micro-services" is not something I would put on my CV at least.

doctor_phil

w zeszłym rokudiscuss

Link to interview with Anders. (linked from the thread as well) https://www.youtube.com/watch?v=10qowKUW82U&t=1154s

comments