Tainnor

> Rayiner takes a lot of arrows on HN because he is (particularly these days) one of a tiny few who is notable for advocating conservative/libertarian positions. Those words in his comment weren't great but they were more of a commentary on society than a personal attack.

Thank you, this reply tells me everything I need to know.

> the way you are engaging with others in this thread

The only person I engaged with negatively here was a person who called me "marinated in liberal propaganda", something that notably you didn't take issue with. I will admit that I should have just ignored that person and will try to disengage in the future. Or maybe just avoid this site altogether.

I did however call out that there's a sizable and vocal minority of users that are very right wing authoritarian and I stand by that assessment. I also disagree that these toxic opinions "rarely get seen", I see them a ton. And my ultimate point is that this serves to ultimately drive away more moderate voices.

Whether or not you consider that to be a problem is up to you.

I hate criminals and social disorder too.

You're part of the problem that I'm talking about. Instead of engaging with the issue at hand, you jump to wild assumptions about my positions, as if there were no alternatives between absolute anarchy and full-on authoritarianism.

That's what I mean by "poisoning the well", you have 124268 karma and yet you can't help yourself but discuss in bad faith.

It's frustrating precisely because even a small amount of bad faith actors can serve to poison the well. It's a problem that ultimately every online community has to deal with in some way.

I'm sure dang will jump into the comments somewhere and point out how HN can't possibly be right-wing authoritarian because of how many people accuse it to be "too leftwing".

The problem is that it doesn't even matter what the aggregate is - even if a bar only has 3 Nazis, it's still a Nazi bar.

And when called out on it reply that the comments are often more interesting than the article which is a) trivially true when you don't read the article and b) probably because bickering in comments is more emotionally satisfying and requires a shorter attention span than reading a rather long article (I'm not immune, seeing as I'm now bickering about the bickering).

Apart from the fact that this was pure self-promotion, it was also spamming the Wikipedias of small language communities with low-effort autotranslated garbage, which I think is rather insulting.

The UK left the EU and is pushing very similar sorts of dangerous nonsense legislation when it comes to the internet, so this is clearly not just a EU thing.

Users definitely care about things like reliability when they're using actually important software (which probably excludes a lot of startup junk). They may not be able to point to what causes issues, but they obviously do complain when things are buggy as hell.

I didn't say complex, I said long.

If you have complex objects and you're doing complex operations on them, then setup code can get rather long.

As someone who leans more towards the side of LLM-sceptiscism, I find Sonnet 4 quite useful for generating tests, provided I describe in enough detail how I want the tests to be structured and which cases should be tested. There's a lot of boilerplate code in tests and IMO because of that many developers make the mistake of DRYing out their test code so much that you can barely understand what is being tested anymore. With LLM test generation, I feel that this is no longer necessary.

It may not be perfect, but IntelliJ beats VS Code on so many other levels that I don't understand why everyone keeps creating clones of the latter.

There have been so many "advances" in software development in the last decades - powerful type systems, null safety, sane error handling, Erlang-style fault tolerance, property testing, model checking, etc. - and yet people continue to write garbage code in unsafe languages with underpowered IDEs.

I think many in the industry have absolutely no clue what they're doing and are bad at evaluating productivity, often prioritising short term delivery over longterm maintenance.

LLMs can absolutely be useful but I'm very concerned that some people just use them to churn out code instead of thinking more carefully about what and how to build things. I wish we had at least the same amount of discussions about those things I mentioned above as we have about whether Opus, Sonnet, GPT5 or Gemini is the best model.

> What appears when you search for it in German?

If you search for "indogermanisch" you're going to get the Wikipedia article canonically named "indogermanische Sprachen" first. The second result I see is the English Wikipedia article called "Indo-European languages" and the rest of the articles also appear to be very scientific.

Maybe the term has some weird connotations in English, but that's certainly not true everywhere and it's also not necessarily true in linguistic discourse because English only became relevant as a scientific language relatively recently (German and French used to be much more common) and there's still to this date a lot of linguistic research being published in languages other than English (e.g. why would somebody who researches the German language publish in English?).

If it had been initially called Indo-Celtic or Indo-Romance and those names had stuck, it would be equally fine, but that's not what happened historically.

You're fighting against windmills, there are no perfect names for huge language families, this gets even worse when we look at certain language families in other continents. It's very common to just pick two subbranches (or geographic regions), combine them and call it a day (e.g. Sino-Tibetan).

> I think most people in the reproducible build space would consider Maven an external uncontrolled input

In an academic sense, you're probably right.

In practice it turns out that this isn't an issue in 99% of cases. Yes, I have once run into a weird issue where Nexus was corrupted and it took some debugging, so it's not like it can't happen, but assuming you don't do anything weird, the assumption that Maven artifacts are immutable is fairly safe.

I'm not saying that lockfiles aren't technically superior or anything, but the failure modes are so rare that people usually don't bother (even in Gradle where lockfiles are technically supported).

Yes, you can, if you manually interact with it. Most people don't do that because why would you? You generally use it as a proxy for maven central and similar and to upload your own internal artifacts through maven-publish. I'm not sure if it's the standard setting, but Nexus should typically be configured to prevent you from overwriting non-snapshot versions.

In a statically-typed language like Java, every class is a type - though not vice-versa, since things like interfaces and records (in Java) are also types.

Non-OOP statically typed languages are basically just saying "ok that's fine, but there's no need to attach state or behaviour to types".

Historically, the term Indo-Germanic was used first, and it's still used prominently used e.g. in German.

From Wikipedia :

> Thomas Young first used the term Indo-European in 1813, deriving it from the geographical extremes of the language family: from Western Europe to North India.[10][11] A synonym is Indo-Germanic (Idg. or IdG.), specifying the family's southeasternmost and northwesternmost branches. This first appeared in French (indo-germanique) in 1810 in the work of Conrad Malte-Brun; in most languages this term is now dated or less common than Indo-European, although in German indogermanisch remains the standard scientific term.

I have no problem saying that Indo-European is a preferable term nowadays, but to claim that the term "indo-germanic" is ethno-nationalist is just absurd. Using two extreme branches of a family to describe the family is a very common practice in linguistics.

Maven artifacts are immutable, so the whole resolution is deterministic (even if hard to understand), unless you're using snapshot versions (which are mutable) or you use version ranges (which is rare in the Maven world).

The effort from going to a paper proof, even one that everyone agrees is correct, to a formally verified one is still gigantic. Requiring all submissions in maths papers to come with a verified Lean proof would be a complete non-starter - most mathematicians don't even use Lean.

In many cases, the problem isn't that the statement of the theorem can't be properly expressed in Lean. It's very easy to write down the statement of FLT in Lean, for example. But for theorems whose proofs have been elusive for decades or centuries, the proofs very likely include objects in rather advanced mathematics that are not at all easy to encode in Lean. This is one of the current struggles of the FLT formalisation process, for example.

In any case, the problem in this case has nothing to do with formalisation, it's simply a case of a bad submission that for unclear reasons didn't get properly peer reviewed.

We won't know if Israel would or wouldn't have been created if the Holocaust hadn't happened, but Jewish immigration to Palestine started much earlier in response to renewed pogroms and rising antisemitism in the late 19th / early 20th century. Already in the 1920s there were tensions and occasional eruptions of violence in Palestine.

> who's opinion on the security of modern cryptographic protocols would you be more willing to follow

I'll follow the people who have actually done work in cryptography. I'm neither under the impression that Wiles himself (or Fermat, if we could resuscitate him!) would have much to say about cryptography, nor do I believe that you have a "simple" proof of FLT.

But in any case you missed the substantial point of my comment: whether or not FLT is true (and no matter how short the proof is) is completely irrelevant to modern cryptography, which relies on entirely different problems (e.g. factoring or discrete logarithms).

Dually, sometimes you'll have something like 1 < 0 as an assumption, which means you can close any goal.

> No more "motive not type correct"

That's exciting to hear!

I have no idea how these things are related.

In any case, to my knowledge, no cipher has ever unconditionally been proven secure except the one time pad. We just have a bunch of conditional security proof that are correct if the underlying assumptions (e.g. factoring primes is hard) are correct. Critically, I think all (?) such proofs only work if P != NP, which still remains unproven.

> 1) FLT may have been proven by Wiles

The "may" is misplaced here. Wiles's proof has been extensively reviewed, just because it hasn't been formalised doesn't mean it's wrong.

> how can cryptography experts expound the security of such and such cryptographic primitives involving discrete numbers, exponentiation, ... but be unable to come up with alternative proofs of FLT? ... but be unable to individually formalize existing supposed proof of FLT? ... but be unable to find a more succinct proof of FLT?

I have no idea why you think there's a contradiction in here somewhere.

I understand what you mean, but I shudder to think at how complicated it would be to write certain proofs without tactics, e.g. simp, ring, omega, linarith and friends all really do a lot of work.

Yes. I've seen proofs fail after a mathlib update because the behaviour of simp changed. I've never seen it do less after an update (so far), but sometimes it'll simplify more and then the next steps may fail to work.

I've since adopted the suggestion (that is afaik used in mathlib) to never use bare simp unless it closes the current goal directly. Instead, if you write simp?, Lean will run the simplifier and tell you exactly which theorems it used (in the form of simp only [...]) which you can then insert into the proof instead.

I would maybe rephrase it as: there are certain axioms that absolutely nobody reasonable takes issue with and then there are others that are more controversial, although it's still important to note that the vast majority of mathematicians accept the ZFC axioms + classical logic.