Hacker News new | past | comments | ask | show | jobs | submit | _flux's comments login

> In contrast, the Rust type system has been mathematically proven to be correct.

Is this the case? E.g. the issue "Prove the Rust type system sound" https://github.com/rust-lang/rust/issues/9883 is closed with comment "This will be an open issue forever. Closing." in 2016: https://github.com/rust-lang/rust/issues/9883#issuecomment-2... .

At least nowadays (since 2022) we do have a language specification for Rust: https://ferrous-systems.com/blog/the-ferrocene-language-spec...


The closest thing is probably RustBelt [0], which proved the soundness of a subset of Rust that included borrowing/lifetimes. This was later extended to include relaxed memory accesses [1].

Neither of these papers include the trait system, unfortunately, and I'm not aware of another line of research that does (yet?).

[0]: https://dl.acm.org/doi/10.1145/3158154

[1]: https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf


It seems though the person who did this repo already violated the copyright by adding these annotations to the source code, correct?

It wouldn't be a reason or validation for others doing the same, of course.

However, whatever one would choose to do, it's best not to do it in GitHub..


The creator of the repository does mention it:

> My hope is that the educational and non-profit intentions of this repository will enable it to stay hosted and available, but the original copyright holders do have the right to ask for it to be taken down, in which case I will comply without hesitation. I do hope, though, that along with the various other disassemblies and commentaries of this source, it will remain viable.


Long copyrights are a cancer in our society. Just notice the fear in his writing - "without hesitation". We're talking about a ~40 year piece of work here.

Patents last 20 years and people keep filing them in the millions. We remain an inventive species. Obviously the protection works. Why do we need to protect copyrights for near a century?


That's not fear, it's an indication of the respect in which I hold the original authors (whom I believe are still the copyright holders). If Bell or Braben asked me to take it this down, I'd roll with it. Same if Geoff Crammond asked me to take down my Aviator and Revs analyses; of course I'd comply. It's their code.

I have copyright content out there in the world (including the commentary aspects of this project), and I'd want to be able to control what happens to that too. Seems fair to me.


I admire your integrity. At the same time, these "rights" come from flawed laws. The code should no longer be "theirs".

I won't write a long and boring critique of the current copyright length, but this work should be in the public domain at this point - nobody should be entitled to ask you to take it down. It should belong to you as much as it does to them. Like Algebra and Hamlet.

It in fact belongs to humanity, as the creation of the work itself was built on top of everything that came before it.


Two reasons: lobbying and the Mouse.

The Mouse has not come back for a third round. Yet.

I don't believe it's completely cloud only, "local control" https://github.com/XiaoMi/ha_xiaomi_home#:~:text=Home%20Inte... sounds quite a bit like non-cloud control?

Could still be behind cloud authentication, though.


Read a little further down:

> Xiaomi central hub gateway is only available in mainland China. In other regions, it is not available.

Nonstarter for many, myself included.

ETA: Yes it does say "partial" local control can be done without the gateway software, but is not recommended and does not work unless you are on the same local network. Better than nothing, but still a nonstarter.


It also says

> If you do not have a Xiaomi central hub gateway or other devices having central hub gateway function, all control commands are sent through Xiaomi Cloud.

Now I don't actually know what central hub gateway function entails :) but it does sound like some non-Xiaomi devices could also fulfill this role.

In case of HASS I think local network is a pretty decent assumption. I have my HASS on both my local VLAN as well as the IOT VLAN.


Hmm, isn't this the definition? 10.3 of https://www.haskell.org/onlinereport/haskell2010/haskellch10...

> The effect of layout is specified in this section by describing how to add braces and semicolons to a laid-out program.

I wasn't going to actually read that in detail to see if it makes any sense, though, but it looks very detailed :).


still people who are touch typists are able to find the characters faster on the keyboard than others. this message is written that way to test that out, in parts where it was possible.

however, in my case the blank keycaps did make the task a bit more difficult. i would write faster in cursive, and it might feel less effort.

also the reason was outlined:

> Allowing the use of (the fingers of) both hands would cause many unforeseen effects on the brain, which would make it hard to interpret the results.

btw, this post was quite frustrating to write.


I don't think that should trigger a reasonable interesting condition one has specified, so that should not happen. So I suppose for non-compiler-bugs you need to check (from the output) that the correct thing is being done, in addition to detecting the actual issue.


Well, that's what I said? If you're "reducing" anything other than a compiler bug (what C-Reduce is made for), you most likely have to execute code.


I was not disagreeing with that, merely pointing out that the reproduction test shouldn't be passing with the minimal runnable C program, or indeed for many many previous iterations before that. In my mind also runnable programs would be tested with grep, instead of relying on the return code of the program.


Well, the conditions were satisfied with pipewire, that introduced some dependency at some point that were not satisfiable in Debian Stable.

So, for now, I'm stuck with the version one commit before that dependency :). (I haven't tried undoing the change later, I suspect it might be dependend upon later on..)


In that case the paid labor loses their livelihood.

What do they lose when they weren't being paid in the first place?


What is the container orchestration tool of choice beyond docker swarm, then?


Is nomad still around?


Thanks, hadn't heard of that.

Seems pretty active per its commit activity: https://github.com/hashicorp/nomad/graphs/commit-activity

But the fact that I hadn't heard of it before makes it sound not very popular, at least not for the bubble I live in :).

Does anyone have any practical experiences to share about it?


Yes have a few Nomad clusters in production and it's been great.

You'll certainly want to combine it with Consul and use Consul templates and service discovery though.

I'd say the difficulty and complexity level is between Kubernetes and Docker Swarm, not having to use YML too is a big benefit imho.


If that's practical experience that you need, I remember reading some studies comparing the reliability and efficiency of nomad vs k8s under load (spoiler: they do not look very good for k8s).

If that's popularity that you need, then sure, nobody ever got fired for choosing kubernetes.


I actually rather like the mli-files. It's a nice file to read, with the documentation and externally available symbols only. However, the fact that the syntax is so different is a bit annoying.

Sometimes I wrote (haven't written OCaml for some time now..) functions like:

    let foo: int -> int = fun x ->
      ..
just to make them more similar to the syntax

    val foo: int -> int
in the module types.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: