Hacker Newsnew | past | comments | ask | show | jobs | submit | c0balt's commentslogin

Or the most likely more expensive rate limiting (computational wise)

I mean, given how the site performs on average I don't think they've optimized so much that the extra cpu cycles of ANDing with the fixed constant of 2^64-1 and then looking up or hashing a 16 byte integer - whatever they do - rather than a 4 byte one would increase the load significantly. Let's be pessimistic and say it's 20 extra cpu cycles, that's not gonna be much of a problem if their load balancers were made in the past 20 years.

That seems a but pessimistic. A few companies use it for customer service, like ime Adidas Germany [0] (they handled an exchange for me once on there). It is effectively just another customer support line like a chat portal on a website.

[0]: https://www.adidas.de/en/help/contact-us


Not really. That is federal spending, right? So your local transport authority or most of the funding of a local schopl, for example, wouldn't be included here?

Lean is far off the most bloated one. Isabelle most likely takes that spot, the main archive includes a whole vscodium among other things.

>> Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three.

> Lean is far off the most bloated one. Isabelle most likely takes that spot.

Among these three is the operative phrase here.

I hate to be pedantic, but we are talking about theorem provers here :)


That is a fair point, thank you for the correction there

I don't know about running per se but practical applications (as in done for product/service) exist. A notable practitioner for Isabelle and Lean is AWS[0]. There is also TLA+ for a more practical tool.

The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation.

[0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.... and https://lean-lang.org/ (Cedar)


That is a surprising sentiment. Most dell and Lenovo laptops work just fine and are usually of reasonably good build quality (non-plastic chassis etc.).

arm64 is however mostly bad. The only real contender for Linux laptops (outside of asahi) was Snapdragon's chips but the HW support there was lacking iirc.


They give us Dell Linux machines from work. They suck so bad and we have so many problems. Overheating, camera is terrible, performance is bad relatively to the huge weight of the device. Everything is a huge step down from Macs.

Whenever I see Linux people comparing Linux and Mac I'm amazed at the audacity. They are not in the same league. Not by a mile. Even the CLI is more convenient on the Mac which is truly amazing to me.


How is the Mac CLI more convenient? There isn't even a package manager in the box, they ship loads of old outdated tools too. Plus there's the whole BSD/GNU convention thing you have to watch out for.

I don't find my ThinkPad running Linux overheats, nor is it particularly heavy. And performance is comparable to the similarly priced MBP at the time. Camera sucks, but compared to my Surface so do the Macs...


Prefer my Konsole setup on KDE and I use both interchangeably all day tbh. Camera yea. The irony is heating issues become less of an issue with arm.

We are lucky in that we can choose our machines (within reason, and no real support if things get broken) and run an arch flavour.

I use thinkpad x1 carbons and have nearly 0 issues. The hardware is not quite as nice as a macbook but it does the job and is nice enough.


Someone's "good guys" are just someone "bad guys". Access to a valuable resource/tool that provides some sort of power and utility will be just another contended item.

> Edit: Maybe this is what github is doing :P

Announcing the new "mobile" tier on azure.


The next step is just selling tickets to that flight in advance as a preorder. One could call it roadster preorders because of the difficult road ahead

Are you sure about that? Flutter development for Android works great in VS Code/Codium. The Android extension [0] for VS Code has also worked fine in the past on a small Java-based App for me.

Android Studio is a probably the best IDE for this usecase but is not the only way.

[0]: https://marketplace.visualstudio.com/items?itemName=adelphes...


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

Search: