skysight-inc/HackerNews huggingface dataset:
TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for Apalache) and your desired properties into an SMT formula, and you let the solver have a go at it. The deal is that the SMT language is quite expressive, which makes such encodings... not easy, but not impossible. And after you're done with it, you can leverage all the existing solvers that people have built.

While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done.

[1]: https://apalache.informal.systems
There’s a scatterplot that’s been circulating on Twitter. The trend lines show that since the time of GPT-2, open weights models have improved at a steeper rate than proprietary models, with the two on a path to intersect.
Game development, maybe. The IoT people just want something to pay their bills.
Not to any reasonable capacity
Provide a link to Stallman using that term then please? Otherwise, I'm calling nonsense. I'd be 95+% sure you're making that up, or confused in this case.
"Requiring the installation of analog AM radios in automobiles is an unnecessary action that would impact EV range, efficiency and affordability"...

I think this bull is them telling on themselves, since the cost of adding an AM radio would be practically unmeasurable compared with the cost of the car. So where would this bill impact EV range, or efficiency, or affordability? The only way this is possible is if the EV makers have to make their cars emit less electromagnetic noise, I'm guessing.
Very nice! Are there any binary packages to test it on Linux/WSL? Have you considered support for UTF-8 half-blocks or Sixel for graphics?
Why scrape profiles when steamcommunity offers a list of selectable countries in the profile edit page?
Why governments need to take a more active role in regulating AI
Why would lower prices be beneficial? Americans already had the highest living standards in the world.
> the culture of the Japanese conservative business owners

Then that 'culture' could use some whacks up the backside, so they don't rootkit PCs and purposely damage CD readers, like that poor kid's portable player going red-hot because of their shenanigans.

Must have been twenty years since Sony got a cent from me, and they're not getting another anytime soon.
Vultures are actually fascinating, team workers that collaborate with crows and magpies to clean the countryside from carcasses.

There is an excellent documentary about this in Spanish: https://youtu.be/4bLO8d0e9O4?si=z2BUAz-90BhWGBdl
This is a great question. In the sense that ROCm is pure userspace it's never necessary - make the syscalls yourself and the driver in the Linux kernel will do the same things ROCm would have done.

In practice if you go down that road on discrete GPU systems, allocating "fine grain" memory so you can talk to the GPU is probably the most tedious part of the setup. I gave up around there. An APU should be indifferent to that though.

There will be some setup to associate your CPU process with the GPU. Permissions style, since Linux doesn't let processes stomp on each other. That might be rather minimal and should be spelled out in roct.

Launching a kernel involves finding the part of the address space the GPU is watching, writing 64 bytes to it and then "ringing a doorbell" which is probably writing to a different magic address. There's a lot of cruft in the API from earlier generations where these things involved a lot of work.

Game plan for finding out goes something like:

1. Compile some GPU code and put it in the host processs
2. Make the calls into hsa.h to run that kernel
3. Delete everything unused from hsa to get an equivalent that only uses roct
4. Delete everything unused from roct to get the raw syscalls

Roct is a small C library that implements the userspace side of the kernel driver. I'd be inclined to link it into your application instead of drop it entirely, but ymmv. Rocr / HSA is a larger C++ library that has a lot more moving parts and is more tempting to drop from the dependency graph.

Going beyond that, you could build a simplified version of the kernel driver that drops all the other hardware. Might make things better, might not. And beyond that there's the firmware on the GPU which might be getting more accessible soon, but iiuc is written in assembly so might not be that much fun to hack on. And beyond that you're on the silicon, where changing it is making a different chip really.
> You are being sold a computer which is controlled by someone else, even after the sale takes place.

Sure, but you are in no way forced or pushed to do that. You only do it if you really want to play their exclusive games. It's a completely free choice in a way that choosing a smartphone isn't (due to various apps being close to required for modern life)

Don't buy the console. Or buy it and something else as well. It's a very fancy toy.
Oh, I think plenty of insiders were calling STS a waste in foresight. I recall a story (no source, sorry) that one of von Braun's people lamented about it: "they've reinvented the wheel, and made it square." Minimum Cost Design methodology for launchers dates from the 1960s.
I'll add my voice to the thankful.
I check (lurk) HN every day specifically because I can find info, tips, other views, and meaningful discussions.
Users here are amazing, thank you all.
Truth tends to take the wind out of hypes sails.

With hundreds of billions on the line for the founders and a whole lot of likely unvested stock options for the employees, it doesnt seem like anyone wants to open up about whats actually going on day to day.
About half of that will go to electricity here in the UK (23.72p per kWh). After costs that's roughly $145 a month profit. Might be more worth it if you have rooftop solar and have free electricity during the day.
Thanks Mike for coloring and shaping so much of what I call my own imagination. I never knew how much I have lived in debt to you.

Rest in peace.
That wasn't really the point of my remark, rather C with Classes C++98 style with plenty of C style coding for strings and arrays (Roman Numerals), Modern C++ best pratices with safety tooling (Arabic Numerals).
It does contribute something though.

One very useful property of flags is that the flag is the same in any language, even if the names for the languages are not.

Having a colorful icon is also helpful if you have problems reading text. Means you don't have to read all the languages' names that are on screen, you can do a coarse visual match by colors and then confirm by only reading the one name.

Modern low contrast monochrome flat UIs are a nightmare for people with reading disabilities and low-grade sight impairment. Speaking from my own experience. A dab of color does so much to help parse a UI. It doesn't have to be the perfect representation or unambiguous. Just give me something to help navigate the UI that isn't just monochrome text possibly with monochrome line-art icons.
The future “Arrowhead/Sony vs Valve Software” litigation is going to be wild
The original concern for shooting down satellites was to stop them depositing material in the ionosphere, the subject of the article.

Shooting down satellites just accelerates the timeframe on which they re-enter and burn up, while making the pieces smaller and hence more likely to completely combust.

That’s counter-productive to your goal.
Well, I'm pretty much okay using fully open Linux called postmarketOS on a smartphone, plus Andbox/Waydroid for (sandboxed!) compatibility with Android apps. That's also a free choice.

On pmOS, there's also full KVM virtualization support (works out-of-the-box on most aarch64 devices) for more picky apps, as well.
> Why do we need all this when we have JavaScript?

In practice, mostly so google can still invade the privacy of users after they disable javascript.

No user ever asked for this.
Come on, they want this to be a PlayStation exclusive because it boosts ps5 sales and everyone wants to have the “hits” only on their platform. they just can’t easily get away with it.

Suuurrree, there are rumours about Xbox (https://insider-gaming.com/sony-helldivers-2-on-xbox/) but I’m gonna go out a limb here and say there’s sweet duck all chance in hell of that happening now.
Probably HTML 4.01 spec.
It’s not an exceptional situation. This is quite commonplace, even in the English-speaking world.
Stripe is here to make it stay. VCs will not let it go.
For a brief moment I thought it was about Premake [1] under a different name, but after checking xmake's Discussions [2] I have found the answer I was looking for.

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

[2] https://github.com/xmake-io/xmake/discussions/1863
Yes and no; think of a loud room where everyone is shouting because that's the only way to be heard due to everyone shouting.
Nothing wrong with books, you just can’t ask them direct questions.
Also, cnn has a similar service just replace www with lite. Such a better experience!
Calorie restriction under the Newcastle Protocol is only required for between 8-12 weeks, typically once you've lost around 15kg on average. Afterwards, it's a matter of maintaining the weight loss through (improved) diet and exercise.
How would flags in the language selection help? The actual problem is finding the language selection at all (which still has an icon of a (stylised) globe on MacOS).
Visa makes double digit $B profit. %100 reason it is not because of fraud. It's the lie they sell you. All card issuers and Stripe too.
> IMO they should either provide the same level of service in all countries, or be forced to charge significantly less when selling their hardware in unsupported countries.

Who would force the price change though?

It seems more reasonable for anyone in a country that doesn't have access to PSN just wouldn't bother buying a PS5 regardless if the price.
I'm not going to change your view, rather I'm going to ask you only realized that now?

I'm not even being snarky. Despite fighting a war for independence, the USA has always loved mom (the UK) and likes its siblings (Canada, Australia, and New Zealand). Five Eyes is probably the most obvious example of our familial cooperation.

The USA will always prioritize AUKUS and Five Eyes before NATO.
Besides flashing your microcontroller, a downloadable executable can (by default) upload all your files to god-knows-where then proceed to encrypt them and hold them for ransom. Also only a .exe for Windows will be provided, good luck running that on your platform.
If you're a Russian speaking Ukrainian, you're speaking like the Russians, which is the sort of analogy I'm referring to.
Exactly. EA would do exactly the same could they get away with it.
You're still essentially using either iOS or Android if you want to interact with many banks. Sometimes they will let you use compatibility layers, sometimes not. (I can't access some bank apps on OxygenOS, which is actual Android)
Rabbit R1 can be run on a Android device
I'd like to meet the person at Sony who thought this was a good idea
> I don't understand why we cant have free flow of people between Norway and the US.

Probably among other reasons is because this would have to be bi-directional and the US has a lot of people and Norway doesn’t want those people coming there.
Or, what happens if renewables fall so much in cost your nuclear plant is cash flow negative?

Following historical experience curves, when the world is solar powered energy from PV will be below $10/MWh.
But if the radio is in a car, it can be moved.

I wonder if the car manufacturers could get around this by offering free handheld AM radios? In bulk, they probably cost less than $10.
The main problem this post complains about is that it's difficult to implement changes correctly, even as an expert. That's definitely not a good thing.
While I watch with some desmay, one of favourite languages turning beyond PL/I levels of complexity, it isn't alone in this direction.

One of the reasons I am not able to follow up on C++ as much as I did in the past, isn't directly related to its complexity, rather that my main worktools, the JVM, CLR and Web ecosystems, are reaching similar levels of complexity, specially with the 6 months release candence, and there is only so much one can keep up with.
> "if you want to interact"

But anyway. I don't want to start the pointless flame war for the milionth time. I think I just have a different definition of "modern life", which is based on using what was considered high-tech not so long ago, like high-throughput radio links and instantaneous worldwide communication (including things like video), without giving up any control. It's not needed to do the abovementioned, so why would I?

BTW, 90% of internet services of any kind still serves "web apps". Which is far from perfect, but gives best compatibility and security out of all technologies we've managed to push to very high adoption.
Ask HN: Is It Worth It?
Just want to talk with community, because can't decide in my head is it will be worth to invest time in a new project or just stop playing in "Entrepreneur' because I'm running over my saving and need start looking for a job.

I have few separate part from different projects, that can be combined

* One is web - Figma like editor with variables, UI https://ibb.co/99GGLRt

* Second is fast and cheep renderer with Cloudflare workers that can use project from that editor

So, my idea was combine them as dynamic image API that will be very cheep and fast. I have did some rough calculation and it can dramatically cheaper than alternatives (Bannerbear, Robolly, Placid and etc, like a lot other and recently launched more here and on PH).
But almost all have about 49$/month per 1000 images subscription. And I bet all using puppiter to generate that. While solution is technically different and my math say it easily can be profitable for me to be like 5$ plan for 1000 images.

I know that it's good to target high priced product and cheep price can lead to more issue with users, and a market crowded with already working solutions...

But, I just really sad to just leave that projects on shelf. But in same time I understand that only advantage here is only price. And as I really suck at marketing, so it will be just like once shoot on PH, etc.

So, I have few question:

1. What do you think? Is it worth to place things together and launch it?

2. Are you using/used such dynamic images api and price issue was a thing for you?

Really happy to hear any thought. Have a great day!
There is WebKit browser in browser: https://trevorlinton.github.io/
> CMake being the standard

Maybe for windows, but I haven't seen it be that popular in the linux world?
You can buy vintage Vereco glassware for 400 EUR/8 pc -- probably less in a thrift store --, or new Duralex glasses for like 40 EUR/12 pc. They're not fancy and they're not expensive. I've stopped doing the party trick of intentionally dropping them to show how sturdy they are because they do break sometimes and it's a huge mess.
I think we need to accept there's no"safe" publishing once the weights are released.

So either we want safe AI and it's behind gated services held by private companies, or it's the complete wild west with open models.

I don't know if they'd any situation somewhere on the middle, and I'm not judging which outcome is preferable, I personally have no clue what's best...
Nop, iPhone is yes or no, consoles are yes, no or yes but without store.

One option more.

The hardware enforced only one store
"One of the important properties of an integer hash function is that it maps its inputs to outputs 1:1. In other words, there are no collisions. If there’s a collision, then some outputs aren’t possible, and the function isn’t making efficient use of its entropy.

This is actually a lot easier than it sounds. As long as every n-bit integer operation used in the hash function is reversible, then the hash function has this property. An operation is reversible if, given its output, you can unambiguously compute its input."

https://nullprogram.com/blog/2018/07/31/
It's possible, see https://github.com/trevorlinton/webkit.js/
True, but probably an experiment that we don’t need to run.
Then it's time for EU to step in
> Then there's death's per kWh,

Given the value of a statistical life (which is something like $12.5M in the US), the value of putative lives saved from going nuclear (using motivated numbers from nuclear advocates) would provide no justification for building nuclear plants instead of renewables. The value would be utterly dwarfed by the excessive cost of the nuclear plants.
Zionists accepted the 1947 partition plan (and as far as I know Peel's 1937 plan to a much smaller territory). The Palestinian leadership rejected both outright.
In addition Zionists proposed the 2 state solution twice (Camp David 2001, Olmert's plan in 2008) to be rejected twice. To this day there hasn't been a clear consent by a Palestinian leader to let go of the Palestinian right of return, nor has there been a prominent Palestinian leader that accepted any kind of border resolution before the Palestinian Nakba. I've never seen it, would be glad to be shown otherwise. So it's pretty much a long trend of Palestinian rejectionism for any kind of solution.

You are cherry picking the facts that agree with your world view and ignoring the rest.
Well it doesn't for me. Just says you can contact support
There is no implicit conversion (except to bool, but that tells you whether the optional contains a value), and operator* / operator-> throw std::bad_optional_access if it’s empty. See https://en.cppreference.com/w/cpp/utility/optional
market reach e.g. ability to have chat app on iOS (the API is less limited)

public relations, limit the edge case nonsense 'journalists' hype so corporate execs aren't terrorized into avoiding buying

doesn't have to be as smart as it could be, it just has to be smarter than other models, so might as well file down some sharp edges for sake of above
The issue with France is that it compete with Us military industry not that it does not produce enough.
It's webrtc, no?
Thanks for the insights, useful. I came to the same conclusion regarding using some CRM platform. I'm a bit surprised I didn't think of that from the get go; might be because I was asked for a completely custom job initially. I've not yet decided on the approach, but currently I'm looking at Baserow[0] and Corteza[1]. I like Corteza's business model much more: allows it to be fully open-source, compared to Baserow's open-core.

[0] https://gitlab.com/baserow/baserow

[1] https://github.com/cortezaproject/
The first commenter on the blog makes a very good point:

> The thing I like to remind people is that this project has been around for decades, during which over a hundred people (or whatever COUNT(*) FROM contributors is) have picked through the code trying to find low hanging fruit to contribute. Everything left to do is astonishingly hard; if it weren't it would have been done already.

There are no easy wins left to contribute.

I've had ideas for a few pg extensions, I wonder if these are as difficult to contribute.
std::optional<std::monostate> has two values, Option<Infallible> has one, so by my counting that's a 100% error.

It is likely the best that can be done, but that's my point, C++ can't do this because the foundational type system isn't up to the task.
Arrowhead has sold out before with e.g. Magicka, so I'm sure they're somewhat used to it by now.

You're not a developer that signs with a publisher like Sony without knowing the risks.
On Steam: If there's little yellow boxes in the right hand column, someone somewhere is reserving the right to ruin your day in some way. Helldivers 2 has three of them: DRM, Third party account, and third party EULA.

Best avoid games with little yellow boxes, especially if you prefer just playing games vs legal drama. (And of course gog.com doesn't have any little yellow boxes)
CHM(computer history museum) have conducted an oral history interview with TSMC found Morris Chang in 2007. Chang told his personal Odyssey in this interview, from inner China to Taiwan, studying and working at US, PhD application refused by MIT, but luckily he choose a fast rocket track in the industry, after he accumulated enough wealth, industry insight, connections etc... He returned to Taiwan to found TMSC, else is the story. Also he compared Asian and American engineering styles:

"I think the Asian engineers tend to be more methodical, they tend to be more studious, more orderly engineers; whereas, the U.S. engineers tend to be more innovative, but they tend not to be as methodical and orderly as the Asian engineers. ......

On the other hand, I also think that one group can accompany another group, you know. You can have an innovative group but not so methodical and so on, and then you can have a methodical group maybe not very innovative accompanying each other.
"

https://archive.computerhistory.org/resources/access/text/20...
We are talking about trillions of tokens.

I’m sure the big players like Google, Meta, OpenAI have used anything and everything they can get their hands on.

Libgen is a wonder of the internet. I’m glad it exists.
And if the "no punctuation" mandate were to be taken seriously, it would also affect innumerable hyphenated names.
>ie, it is common enough that we have a label for it.

Having a label for something doesn't imply that it's common. We have labels for plenty of rare things as well.

Also, "mental illness" is a far more broad category than what's being discussed, which is specifically symptoms that resemble the hallucinations and confabulations of LLMs, at the frequency with which LLMs display them. Most mental illness doesn't involve hallucinations or confabulations That is not common in humans, in LLMs it's normal.

>If you put a little fence around the people hallucinating and dehumanise them then sure, humans don't hallucinate.

I'm not dehumanizing anyone, this isn't a rational argument, it's just an ad hominem.

> The problem with that argument is they are actually still people.

The problem is that isn't the argument, and you can't attack the argument on its merits.

The simple, plain, demonstrable non-prejudiced fact is LLMs confabulate and hallucinate far more than human beings. About 17% to 38% of normal, healthy people experience at least one visual hallucination in their lifetime. But hearing voices and seeing things, alone, still isn't what we're talking about. A healthy, rational human can understand when they see something that isn't supposed to be there. Their concept of reality and ability to judge it doesn't change. That is schizophrenia, which would more accurately model what happens with LLMs. About 24 million people have schizophrenia - 0.32% of the population. And not even all schizophrenics experience the degree of reality dysfunction present in LLMs.

You are claiming that, in essence, all human beings have dementia and schizophrenia, and exhibit the worst case symptoms all the time. We wouldn't even be able to maintain the coherence necessary to create an organized, much less technological, society if that weren't the case. And you're claiming that the only reason to believe otherwise must be bigotry against the mentally ill. Even your assertion upthread, that "a lot of the most intelligent humans turn out to be crackpots" isn't true.

Stop it. Stop white knighting software. Stop normalizing the premise that it isn't worth being concerned about the negative externalities of LLMs because humans are always worse, and thus deserve the consequences. The same attitude that leads people to state that it doesn't matter how many people autonomous cars kill, humans are categorically worse drivers anyway. I can't think of many attitudes more dehumanizing than that.