HN user

doctor_phil

112 karma
Posts1
Comments36
View on HN

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.

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.

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.

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?

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.

Lil' Fun Langs 5 months ago

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. :)

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.

Why does the fix need to remember all the nodes we have visited? Can't we just keep track of what span we are in? That way we just need to keep track of 2 nodes.

In the graphic from the example we would keep track like this:

  low: - high -
  low: 11 high: -
  low: 23 high: -
  low: 23 high: 26
  Error: now we see item 13, but that is not inside our span!

We have a hard time understanding what dark matter is. There are theories that some of the dark matter could be tiny black holes left over from the big bang, called primordial black holes (PHBs).

How can we detect PHBs if they exist? If they existed in large numbers, would we notice them? The paper says that you would notice a PHB if it went through you, since you would likely die. We are not noticing people dying by mysterious gunshot-like wounds without guns in any large amounts, so there can not be that many PHBs around.

The paper is (weak) evidence against a large amount of PHBs. The paper is also slightly funny.

I actually haven't tried Nix (or other nix-alternatives) yet. I've seen a lot of complaints about the language, but a lot of praise and love of the idea. I though Guix was the "main" competitor to nix, using a more mainstream language (Scheme). Is that still the case? How would Brioche compare against Guix if you are OK with both Scheme and Typescript as languages?

Preventing accidental privacy intrusion is easy. If you have a fence around your property (or even something as simple as a mowed lawn) then it is quite obvious where your plot starts and where the forest ends.

Someone malicious doesn't care about laws anyway. If they get caught today, couldn't they could just deny that they were there? I don't understand what would change in that case.

The point is that every function is explicitly telling you if it can or can not return null. Your editor and typechecker will tell you if you need to handle null after calling that function.

If you have a non-null returning function that you need to change so it can return null, then your typechecker will tell you all the places where you now need to handle the new null return.

It doesn't need to be a very large codebase before this becomes a very useful tool to help when refactoring.

But a switch and an if-else *is* a matter of algorithmic complexity. (Well, at least could be for a naive compiler). A switch could be converted to a constant time jump, but the if-else would be trying each case linearly.

I found this book very helpful as a supplement to "Crafting Interpreters". The BEAM has a lot of interesting features that many mainstream languages don't. I found the parts about processes, tagging, memory and reduction counting (chapters 3-5 and 11) especially interesting.

The book is clearly very unfinished still, but what exists is very good. Got my mind spinning on what a good statically typed language running on a VM could look like.

I think you read parent-comment wrong. My interpretation: unlock your phone normally at least every 12h. Only if you fail to do that, then the phone locks harder and you need to unlock with the non-memorizable password. Imagine the PIN/PUK system on SIM cards but with a timed lock-out as well. I agree that it sounds inconvenient though.

I'm not that familiar with the US law system, but wouldn't a written down password be worse? With a memorized password it's at least possible to claim you have forgotten.

Some encryption schemes allow two keys for unlocking, but they would show different content depending on the key. I think I remember trying that on TrueCrypt many years ago.

How big a factor is the rotation of the black hole? Maybe look for a large black hole not rotating too much if you want to be sure. :-)