someplaceguy

> Is there any reason to use SML instead of OCaml in 2024?

* Many compilers and transpilers available. Don't like LunarML? Maybe try Poly/ML. Or MLton. Or MLKit. Or SML/NJ. Etc. All of the above are pretty much complete and production quality, and there are quite a few more.

* The language has a formal specification which means there's a document formally specifying what all the constructs in the language should do. In contrast, if you wanted to build your own OCaml compiler/transpiler/interpreter, you'd basically have to follow whatever the main OCaml implementation does, which changes from one version to the next, so you'd always be playing catch-up.

* The formal specification hasn't changed since 1997. This means that once written, your SML code should work the same forever. You no longer have to worry about your programs (or their dependencies) breaking when you upgrade to a new version of OCaml.

* Compared to OCaml, your single-threaded programs will usually run faster if you compile them with MLton, mostly due to whole-program optimization / monomorphization and unboxed native integers, reals and arrays.

* Some SML implementations have interesting extensions, which you can use (at the cost of being tied to that implementation). For example, MLKit supports memory regions (i.e. more efficient memory management in some cases). SML# (which is not related to .NET) supports seamless integration with SQL and other interesting features. Some implementations support multi-threading natively and/or different forms of parallelism. Most of them also support some form of FFI to interface with C or other languages.

* SML programs are easier to port to CakeML than any other language, since CakeML is mostly an SML subset. CakeML not only allows you to formally verify that your program is correct (or that it has certain desirable properties), but it also has a compiler that is formally proven to be correct, so your compiled CakeML programs are (mostly) guaranteed to be free of miscompilation bugs as well.

> you can make 2 GPTs sing just as easily as you can make 100 GPTs sing.

> What can you do with a billion GPTs?

The world's largest choir?

I've lived in 3 EU countries and visited and known people from many more and while it's true most people would be against most wars, I don't think most people would be against a MIC sponsorship for an open source conference.

Airbus alone employs 40,000 people in the defense sector and there are many, many more MIC companies in Europe where many people are happy to work at (for the record, I'm not one of them). Also, all European countries have a military and buy weapons, and probably all of them also manufacture some weapons or others (microstates being the exception). Some of them even have mandatory drafts, I think.

As an example, I'd be shocked if an Airbus sponsorship would ever be rejected in Europe (perhaps Germany being the exception now that I'm familiar with the Civil clause).

Honestly, you sound like someone with a heavy anti-US and anti-MIC bias (and admittedly, I'm also known to take pleasure in anti-US and anti-MIC prejudices, but my concerns don't intersect this particular scenario at all).

> Sponsorship with the attached advertisement is very different than "used by". Don't be silly.

Sure, but what does that have to do with the Civil clause that you mentioned? It doesn't say anything about sponsorship, but it does say about "used by": "Any participation of science and research with military use or purpose must be rejected". Obviously, this cannot be true, since it can be applied to anything that is used by the military, including paper, towels, pens, computers in general, water, etc.

> Are you even aware, I am referencing the issue of a Nix conference hosted at a German university

I am, and? I think you missed my point?

> I linked a Wikipedia article, read it, if you're genuinely interested and not debating in bad faith.

I did. The Civil clause of some universities does sound fine ("strive to", "focused on"), but the others make a blanket statement that is very hard to take seriously. Obviously, they don't take the statement to the letter, and in fact it's hard to tell what they aren't supposed to do (if anything), unless perhaps you look at the other universities. Even then, none of those clauses say anything that can be applied to hosting a conference with military sponsorship but not to contributing to Nix.

Regardless, I don't think what you linked to is well known outside Germany. You can judge by the extent and completeness of that Wikipedia article. I'm European (EU), went to a European (EU) university and I had never heard of such a clause.

To answer to your point:

> To even think of the sponsorship as a valid idea is US centric ignorance. Outside the US people don't get the "Thank you for your service" indoctrination and are way, way more reluctant to work with the MIC.

I think you're generalizing a wee bit too much -- I'm not from the US and I think there's plenty of indoctrination to go around, and yet I don't think rejecting this sponsorship is in accordance with open source and Free Software values, philosophy and spirit. You can go read about it here -- and notice how it says several times that the point is to include everyone: https://www.gnu.org/philosophy/free-sw.en.html

To be honest, I think the mistake with Nixcon was not Anduril, but rather, to host the conference at a German university.

> perhaps we do need a new popular license or set of variants that exclude certain industries.

Such a license would not be considered open source or Free Software.

Someone else posted this link about a similar situation in the past: https://en.wikipedia.org/wiki/Douglas_Crockford#Software_lic...

> In particular the civil clause demands that members of the university reject research projects and funding which could serve weapon technology.

Wait, what? Are you saying German universities are forbidden from contributing to Nix/NixOS, which is used by Anduril?

Or say, the RISC-V ecosystem, which may be used as chips driving military weapons?

... or the Linux kernel? Heck, any OS at all?

Oh God, imagine the self-, peer, and top-down pressure to take that, both for students and working adults.

May I ask about your experience since leaving Ozempic compared to before you started taking it?

I'm not considering taking Ozempic nor am I aware of anyone who has, so I'm curious.

Yes, but the hard part is that were a lot of "74"s and you had to figure out which one had to be changed... :)

> Could have been summarized as "I'm okay with my software being used to kill people and taking money for it".

I don't understand. Are we supposed to start policing who is allowed or not allowed to use open-source and free software projects, which goes against these licenses themselves and their requirements?

If you're against the NixOS Foundation taking money from Anduril, would you be opposed if the NixOS Foundation accepted the money and then would donate it back to Anduril? Because that would be functionally the same as not accepting the money and yet by your line of reasoning, it seems like you'd object even more to that.

As far as I understand, the formal objection that was posted on another comment/thread was to the NixOS foundation advertising Anduril (not taking money from it or accepting contributions from it), which to me makes a lot more sense even though I don't have a strong opinion about it.

I'll happily concede the expensiveness point, and also say that if we are not entertaining the idea of forcing anyone to give up meat (which is what I thought we were discussing), then we are not in disagreement.

I'll only add that when promoting vegetarianism or veganism, I find most such sources to be akin to propaganda, i.e. they always talk about the benefits but rarely talk about the disadvantages. I suspect this might be because veganism is often tied to political preferences (and certain cultures).

As an example, here's something Wikipedia mentions that you will not usually see entirely discussed in articles promoting such diets:

> [Vegan diets tend to be lower in] omega-3 fatty acid, vitamin D, calcium, zinc, and vitamin B12. As a result of the elimination of all animal products, a poorly planned vegan diet can lead to nutritional deficiencies that counteract its beneficial effects and cause serious health issues, some of which can only be prevented with fortified foods or dietary supplements

This might partly explain why it's about as common to find a vegan bodybuilder as a flying cow... it might not be impossible to find one, but it's about as unnatural. And there are probably good reasons for this, including availability and easy absorption/digestibility of all the essential amino acids, which is important for muscle growth and maintenance, which in turn is very important for health especially in middle and old age.

It could also explain why when I see a random vegan person, they tend to "look" unhealthy more often than a random non-vegan person, although I concede that I may be biased, of course -- I've also seen sources claiming vegan people live longer, although I suspect that if it's true, it may be because vegans tend to be more health-conscious and choose their diet and sources of nutrition more carefully, not necessarily because of the lack of meat itself.

But of course, as long as all such information is reported in an unbiased and accurate fashion, I see nothing wrong with it.

> If you take the meat out there's a whole world of nutritious and delicious foods out there.

But most people will not find, enjoy or choose food with both of those qualities, not to mention that they are a minority over what's commonly available -- and even if they are available, they'd probably become too expensive if consumption increased significantly.

Most of the time they'd have to choose between "delicious foods" or "nutritious foods", but not both, and you know they'd choose the former.

If you take out meat, you'll simply reduce the pool of available (good) choices. You'll have a strictly worse outcome than what you had before (except for the animals, admittedly).

> That means the obesity isn't due to meat or a lack of meat, per se. It's the diet outside of the meat.

So... if you take the meat out what does that leave you with?

They also didn't eat a lot of fries, sugared beverages, ultra-processed food, etc... which is easily available nowadays and likely to be consumed when one doesn't feel satiated (e.g. due to meat consumption).

That's not to say that there aren't alternatives to meat that also satiate and are nutritious, but most people don't consider them to be equally delicious and therefore they are not as likely to be consumed if meat isn't available.

> half of the planet is overweight/obese, I think we could slow down a bit tbh

I don't think half of the planet is overweight or obese due to meat consumption.

If anything, take away the meat (or make it more expensive) and it'd probably lead to even more obesity.

> I think you’d have a hard time aligning the amount of the paycheques such that the puppets couldn’t get bigger expected future paycheques by doing what they wanted with tiktok.

Presumably the puppets wouldn't have access to the tiktok platform (its code including AI algorithms, data, employees, etc), they'd just be a middle-man that would take the finished product (e.g. the APK) and publish it to distribution platforms (Google and Apple's app stores)?

> The second one is WOW.

Indeed! Now assume that the many-worlds interpretation is accurate and you will live through most of that, if quantum immortality [1] turns out to apply to the real world.

[1] https://en.wikipedia.org/wiki/Quantum_suicide_and_immortalit...

I should note that I'm not a computer scientist and I'm currently a bit sleep-deprived, but to continue discussing what you're interested in:

I tend to think that an efficient computation of some finite-state version of Kolmogorov complexity would necessarily require an efficient computation of a finite-state version of the halting problem, but I'm not entirely sure of this.

Naively, it seems that this Kolmogorov calculation would require enumerating all programs (in increasing program size) and then running each of them until they either 1) enter an infinite loop, 2) produce the input string and halt, or 3) start producing a different string.

However, I'm not sure this would be the most efficient algorithm. For example, it might be easy to inspect each program and discard almost all that would "obviously" not produce the input string before we even try to run them.

Or better yet, never even enumerate such programs that can be proven not to produce the input string. In other words, cut the search space significantly.

Perhaps there might even be a shortcut to directly construct the smallest program that produces a given string, or at least, a family of small candidate programs that would be a very small subset of all possible programs and yet would be guaranteed to contain the solution.

As you might have noticed, unfortunately I don't know if there are such extraordinarily efficient shortcuts, I'm only speculating that they might exist.

That said, I still suspect that this might be intractable due to having to account for the worst case, i.e. undecipherable random-looking programs. In the case of the halting problem in the context of formal verification, I'm more optimistic since we usually don't need to care about such random-looking programs, only human-constructed ones (usually), which might be far easier to analyze algorithmically. I don't know if that makes sense...

I would somewhat agree with your comment, but I think you're missing some important points:

> everyone understands that "exponential time" is still "never" in practical terms.

It's important to note that this is not necessarily true:

1. "exponential time" is somewhat ambiguous. An algorithm might be exponential time yet have a very low exponential base (e.g. 1.0001), so in practical terms it might be practically computable for reasonable sizes.

2. Even if the exponential base is high, it still doesn't say anything about whether an algorithm can be used practically or not. The algorithm might still be very efficient for reasonable problem sizes even though it has a high exponential base (important question: exponential in terms of what, exactly?).

3. Exponential time algorithms might only be so in the worst case but might not necessarily be exponential in the average case, or even the vast majority of interesting cases. As an example, it might be easy (or at least doable) to solve the halting problem for normal computer programs. Humans do this all the time with real-world programs when performing formal verification (as these programming languages, logics and tools force you to prove that loops and recursive functions always terminate, even when assuming a model equivalent to a Turing machine), and AFAIK there's no proof that computers can't efficiently do the same for the vast majority of real-world programs (cryptographic algorithms being the usual exception).

4. Whenever someone mentions that the halting problem and Kolmogorov complexity are uncomputable, the discussion ends there. But notice that when I pointed out that it's in fact computable, the discussion turned into one about how efficient the computation might be (which I argue, is how all such discussions should be).

5. As a side note, every single time I argued this point in the past, usually in the context of the halting problem, someone always argued that such an algorithm would necessarily have a time complexity of 2^N, where N=nr. of bits of the machine. This is not true. It would only be true for the simplest and most naive solution to the halting problem, which is inevitably what that person has in mind. In fact, there's already a family of algorithms that solve the halting problem with less complexity for almost all programs: "Floyd's tortoise and hare" and similar ones (see [1]). Note that these algorithms don't even inspect the program, they just run it step by step. This leads me to think that there are undiscovered algorithms that are far more efficient by virtue of exploiting knowledge about the program being analyzed.

[1] https://en.wikipedia.org/wiki/Cycle_detection

> Unfortunately, that's uncomputable

Minor nitpick, but while Kolmogorov complexity as typically defined is uncomputable, I would argue that this result is only a theoretical curiosity and mostly irrelevant.

That is, the "uncomputable" Kolmogorov complexity computation presupposes that you have a Turing machine, i.e. a machine with literally infinite memory, which is not possible to construct in our universe. Or alternatively, it presupposes that "computable function" is one that can be computed by a machine with an infinite amount of storage, which amounts to the same thing as having a Turing machine.

You could probably define some version of Kolmogorov complexity that is parametrized by the memory size (e.g. of a linear bounded automaton or similar model that better represents a computer with finite resources), which should make it computable. That said, in practice it would probably take an unreasonable amount of time to perform this computation (but that is orthogonal to whether it's computable or not).

According to the formula you'd have to divide by 2*N.

> So for instance a thermoelectric generator operating between 25 °C and 5 °C has a maximum efficiency of

> Eff = (298 - 278) / 298 = 6.7%

Does that mean a thermoelectric generator operating at a minimum of 0K has a maximum efficiency of

Eff = (N - 0) / N = 100%?

Will that stop other people from tracking my devices?

Or will they still send my location and Bluetooth ID information to Google?

First of all, I said it's not possible currently. Which is what I'm interested in. Not that it might not be possible in the future if enough pressure is applied (that might be interesting for activists, which I am not and have no interest in being).

Second, it's not mine or EFF's responsibility to police what Google does. Let's make it very clear that the current situation is Google's responsibility and nobody else's.

Third, it doesn't matter whether I stop using Google services because other people using those services will track me anyway.

And fourth, what does it say about a company that you can only use its services if you agree to be tracked and agree to track everyone on the planet without their explicit consent?

I mean, let's be clear here. This is not "I'm tracking a pseudonymous ID across websites". This is literally tracking the physical location of someone whose real ID Google can easily find out, through a wide variety of means.

Even Google has to comply with warrants. Even secret ones.

You should assume the location of your devices will be disclosed whenever the US gov has a plausible reason for requesting it, regardless of which part of the globe you live in.

So you're saying that it's not possible to do what I asked, currently.

And judging by the other comments in this thread ATM (with one possible exception), nobody seems to care...

Let me qualify my question: how do I disable this completely without otherwise losing network connectivity or other features?

i.e. how do I opt out of tracking other people and being tracked myself, i.e. without explicit consent?

Sure. But more importantly, how do I disable this completely?

The military format is ambiguous. For example, 12MAY24 means 2024-05-12 in English but it means 2024-03-12 in Manx Gaelic [1].

Also, tell me: what date is 10SKÁ11? Or 01DU02?

Furthermore, a lexicographic sort will do the wrong thing.

Better stick with ISO 8601.

[1] https://gv.m.wikipedia.org/wiki/Mayrnt

Clang has a similar tool, the Clang Static Analyzer: https://clang-analyzer.llvm.org/