skysight-inc/HackerNews huggingface dataset:
> The real future though is theorem proving systems, and generating code from them.

I've heard the same thing about model-driven development 25 years ago. Outside of some very small niches, it's pretty much dead now.

> But theorem proving systems that embrace the full spectrum of abstract and correct thought.

And here's where reality and the ideal world collide: the vast majority of applications consists of incomplete models (in that data and/or understanding of the problem are incomplete), quickly shifting goals, and pressure to release.

Theorem proving systems offer nothing that helps with this class of software - abstract and correct thought sounds marvellous in an academic environment or if you have unlimited budget to hire top talent and perform thorough analysis.

In practice, however, your typical line-of-business application is faster, cheaper, and well-enough programmed using traditional languages and a healthy dose of best-practises.

Optimisation and platform support are another area where a TPS won't be very useful. Every hardware has its quirks and workarounds are required to get the best performance or avoid pitfalls. These aren't easily expressed (and identified) using abstract thought and models.

Last but not least, no sane company is going to just throw away decades worth of investment in applications, libraries, and (software-)infrastructure just for a nebulous promise of what basically boils down to smarter and better staff with the right tools.

Theorem proving systems have their place and that place might get bigger in the future, but they're most certainly not the panacea of all software development.
You will be disappointed. It is abundantly clear that it is about bullying for favorable coverage as opposed to actual facts of the matter. When evaluating people don't listen to their nonsensical mouth-noises look at what their actions say - attacking information sources around election time and going after the ones with no barriers to entry - they don't even need to be in the country to compete! Ignoring the ones with actual legal monopolies granted to them.
Haven't seen this discussed on HN, and seems like huge news.

Why isn't this more known? Is it moving forward? Has it been announced officially...
Antitrust enforcers care about anticompetitive behavior not monopolies. They certainly should care about rent seeking behavior that Apple is engaged in.

Saying something is or is not a monopoly is distracting from what actually matters. It's deflecting.
Again - WhatsApp, Apple, Telegram and Signal _are_ indeed service providers. Matrix is not.
Politicians only think short term
Kiwix lets you access free knowledge – even offline
Exactly. Sorry about that, should have included this one before sharing it here. I have font-size support for version 2.0, but I might be able to update the tool during the weekend to add font-size and a couple more minor issues.
I don’t know much about Spain or Italy, and I agree that Germany uses a lot of copper cables. But France and Poland? Esp. in Poland it most towns you have fiber, all new buildings have had fiber for ages. I currently pay 15–20€ / month for 1Gbps in a like 5th biggest city in Poland (not center, but not far either). In a couple of places in France I’ve stayed longer the internet was good as well (though I don’t recall the prices or exact speed details) — cities including Paris and towns. Granted this is all anecdotal and my bubble, etc.
But if you are stoic it is not the offenders fault either. You are only promised suffering and it is up to you to manage that suffering. Maybe nobody on HN wants to be a stoic.
I'm a fellow fan of antlr but it's not really an option for the base interpreter. They're (rightfully) very stingy about deps. cpython supports a wide range of platforms and has its own very permissive license - it's a pretty self-contained codebase and they prefer to keep it that way.
Well, the details remain to be finalized but the general idea is a generator DSL. Think of HAML in regards to HTML for example: you can write nice DSL-specific code that gets translated into valid HTML code. (There is already a relevant module for that for Arturo, thought at a very experimental level: https://github.com/arturo-lang/art-html-module).

I'm thinking of the same thing for LaTeX (and perhaps even more sophisticated). One of my main "businesses" is centered around typesetting and electronic publishing, hence I'm a heavy ... LaTeX user.

Feel free to ask anything else. All suggestions and contributions are welcome! :)
It seems reasonable to assume more money = better in replying to a comment that brings up the monetary amount in the second sentence? If they have their own clinic to enjoy life better, great, but in that case trying to compare revenues doesn't seem like the relevant thing to do.
The Wonderful World of Modified Game Boys
You are realizing the huge amount of control you are handing over in this dialog compared to quickly scanning a list of potential shows and being able to quickly scan available seats and prices?

Information is power and these chat interfaces will sooner or later prey on the less informed.
A brief introduction to BEAM
A new programming language and tools for fact-checking
>And why didn't Facebook get sued too?
>And what about Amazon?

I completely agree, and this has been my main headscratcher since we first heard about a possible anti-trust case.

For starters, I still think things like banks, telecom, and probably oil, and defense industry companies probably need to be broken up, and that they should be much higher priorities. To say nothing of the obscure industries we wouldn't normally think of (Luxxotica with glasses) that are monopolized. There's probably others for obscure things I'm not even thinking of.

And even within tech, I wouldn't even rank Google ahead of Amazon, and I'm not 100% that I would rank them ahead of Facebook either.

And, if that's not all, I think Google at least serves as a check on the other Frightful Five, and subtracting Google will serve to further consolidate tech. And if that's not enough, I feel that the tech industry has served as a useful check against other entrenched industries. Their clash with cable, and occasional work to protect an open internet are a healthy counterbalance to voices of other monopolized industries.
Free markets seem to have like a metaphysical power to people who hold the above opinion.

Even if the above was true, wouldn't someone in a free market be free to form a monopoly if they wanted too? What would prevent them? Other people trying to form a monopoly? How can you assume they wouldn't just give up? It's basically just a faith based belief that someone will always be around to compete against the monopolists. Surely the average citizen has something better to do.
Hey guys, I'm super excited about early access so that we can gather as much feedback as possible. We made a nifty handbook [1] a while back to show the basics of building a page in Makeswift. Would love to hear what you think!

[1] https://www.makeswift.com/handbook
Farmers stick with Trump, despite trade-war pain
AG Barr has been pushing to get this out before the election, over objections of his own attorneys:

"He [Barr] pushed career Justice Department attorneys to bring the case by the end of September, prompting pushback from lawyers who wanted more time and complained of political influence."[1]

[1] https://www.nytimes.com/2020/10/20/technology/google-antitru...
This is on my todo list. Will add this one soon (maybe next weekend)
This is a very well written post and I'm happy Matrix is taking this seriously.
Ah yes... the ‘80s and the end of the USSR have sadly wiped out most intellectual discourse on the prime principles of society, from a mainstream perspective.
I tried it on Firefox 79. The menu would show various emoji, but selecting one would sometimes use the Unicode version rather than the exact style that I selected.

For example, the laughing with tears emoji is in full color with an open mouth, but selecting it results in the outlined version without color and is showing teeth.

When the colored emoji do work, they will sometimes be cropped at the bottom or will leave some artifacts behind from a previous selection. These seem to disappear when switching to another tab and then coming back, though.

Some of the letters will extend beyond the boundaries of the image, too. For example, the left and right ends of the combinations "me" or "ww" get clipped off.

Despite those issues, this looks promising. I really like the interface and overall simplicity of the tool.
How am I down voted for saying what they are saying is stoic?
Why should it matter that cost of living varies?

If you move to San Francisco, you should know that your money isn't going to go as far; conversely if you move to Tulsa you should reasonably be able to take advantage of the low cost of living to build up your savings. If you're residing in Tulsa and still only just surviving, you're not earning a living wage.

Then there's the fact that besides food and rent pretty much everything we buy nowadays is nationally priced - amazon doesn't give you a discount for moving to a low cost of living area; and you don't get to pay lower taxes because cost of living is higher.

But beyond all this, the disparities arise almost exclusively because of a few outliers - maybe 5% of people in the country can live comfortably on less than $20k/yr and less than 10% require substantially more; the vast majority of Americans are close to the average.
Generate Dynamic Opengraph Images Using Gauguin
30% from app stores is the norm for app stores that have market power in their respective markets, but all that tells you is that's the amount of the monopoly rent. Compare this to the Microsoft store, where the store itself doesn't have market power, and then they don't take 30%:

https://9to5mac.com/2019/03/06/microsoft-store-revenue-share...

But still 30% for XBOX/games where they once again have market power in that market.
Some countries can have blurry lines between companies and non-profits; in this case, Matrix.org is a Community Interest Company in the UK (https://matrix.org/foundation), so I assume that'd apply to it as well.
> In my experience, 9 times out of 10 delegating sections of content with a final edit and sign off by a designated individual would work very well - no real time collaboration needed.

So that's actually how we do our internal weekly presentation. Each team has a section, and we all work on it. (Albeit in realtime)

> no one is really sure when a slide is finished

You can assign slides in pitch and update their status. So everyone knows who is responsible for something and what state it is in.

https://help.pitch.com/en/articles/4318642-set-a-status-and-...
Right, but now my username gets taken and I don't get any notifications or can send images on this service???

Any big service will require multiple security checks, after you sign up to Discord, you can login with a QR code on a new device. No captchas. and get the above for free.

It is going to be a mission to get a bunch of friends to use this 'Freenode' service.
Azure ML Studio is a good tool for your non-data-science developer to play around with ML tools. I picked it up at my company and it was fairly easy to make models and predictions with.

Of course, once you actually start to get good at it you want to switch back to using code, but it's a good way to start.
How does it add burden when reading code? Writing code, sure, but only when you don't research the environment you're going to be deploying into. Unless you started working with Python like last year you probably remember when new useful features were released, and for stuff you haven't used before, the Python documentation always tells you when it was added.
People using numpy are not in the fringe. If this wasn’t triaged during prereleases then it’s either that it doesn’t always cause problems, or there is an issue in the diversity of testers.
I wonder if a good hack would be to think in terms of how I would react if a (my) child showed me something they made? Children are often doing something for the first time. I've noticed this breaks down my barriers to what I consider impressive.

Founders are in a similar situation, but since they're almost universally adults, we tend to apply adult prejudices to their work.
Facebook is a viable alterative to Google from an advertising perspective. This action is taking place despite there being far more competition in search and advertising than there is about the abuse of code signing permissions by Apple.

Antitrust action has never required the lack of an alternative.

> FB is being used by foreign powers to shape US elections, and you think Apple is the biggest problem here?

Apple is being used to attack democracy campaigners in Hong Kong, mainland China and Belarus, and has a long history of attacking sexual minorities and sex education efforts.

Yes, Apple is 100% the biggest problem here.
Did Azure Notebooks have anything proprietary beyond Jupyter notebooks? If not, not a huge deal - can still take away all of your content and rerun elsewhere :)
Hi HN!

Most of us want to do more in the battle against climate change - it’s tough when your work life is unrelated. Right now, if you want to find a job that helps the planet, there’s no clear way to go about that. You could look for environmentally focused companies individually and keep checking their site to see if they are hiring. But that’s tedious and it’s easy to miss new postings. Conventional job boards don’t have a good way of filtering for this. A couple of environmental jobs boards exist, but they have low post volume and are dispersed geographically.

https://enviro.work is the place to come find green jobs in one spot. Think of it like a search engine for all Earth-friendly jobs out there. We aggregate eco-positive jobs from different sources and link you back to the source.

We wanted to help empower purposeful individuals to maximize their potential for the planet. Enviro.Work is linked with the community at https://collective.energy, where you can find inspiration, feedback, and an audience for your eco projects. Turn climate ideas into plans into reality - then build your team with Enviro.Work.

I'd love to know what you think and hear your helpful feedback.

Thanks for caring! Eric (Enviro.Work maker)
Realistically I don't see forced break-ups being in the cards here. That hasn't happened since, what, AT&T, decades ago? My guess would be it's all consent decrees -- what they hit Microsoft with, and what they could hit Apple/Google/Facebook/Amazon/Microsoft with now.
It's not any more suspicious than announcing it 3 months earlier or 3 months later.

There is no right "non-suspicious" timing for this type of scrutiny.
Beta tester here. In love!!!
Direct-to-DOM commenting. Install/setup in seconds. Your projects now have a "comments layer" on top of your views. No more out of context feedback.
Thanks for making this!
Hmm... I had no idea. Thanks a lot for the suggestion :)

P.S. A little bit of trivia: my choice of the scorpion logo was no random selection at all. Arturo was my little (well, not so little) Black Emperor scorpion that passed away in February. Hence, the name. And the logo...
How do pandas DataFrames work? (kinda)
“Without backdoors” wow, shots fired at Moxie “federation won’t work” Marlinspike’s secure honeypot Signal.
Yeah, the dropdown is not very well accessible. I'll use another autosuggestion component or improve this one for the next update.
Google's business is ads, not search
Could there be political motivations in politics? I'd expect so.

The issue with doing anything during an election is that people on the other side accuse the administration of suspicious timing. The issue with doing nothing during an election is that everyone accuses you of being a lame duck. This is, more or less, business as usual for the administration; they've been on Big Tech's ass for at least a year now, and finally something is coming of it.

Every big tech company needs looked at, and potentially split up. And, maybe, they'll all get their turn. But resources are limited; when the US went to war with Germany, we didn't airdrop troops in Berlin, Hamburg, Cologne, Munich, and Frankfurt on the same day. Actually, we didn't even start with Germany. Starting with Google allows some legal precedent to be set on some of the very weird, novel antitrust issues the case is going to face, which will make future cases easier. I tend to think Amazon should have been the first, but Google is certainly up there, and probably (IMO) a more potentially harmful monopoly than Apple, Microsoft, or Facebook.
Ah, HN's Dustin Curtis phase, like snap bracelets and pogs.
>customers don't actually pay for the products and services

By the plain language of this, it would apply to privately insured patients as well. No matter how pricey the plan, it's the insurer that controls how much is paid, not the patient -- and their incentives are to promise a lot, and then pay too little to cover it.

So, is a private insurance+hospital system likewise doomed to "go downhill"?
in systems where reputation has significant monetary value, how do you stop people from exchanging money for reputation? it's a serious problem which i've never seen solved when participants don't have trust established with each other, e.g. amazon reviews are completely off the rails, but HN karma works quite well. slashdot has metamoderation which i haven't seen implemented anywhere else - it seemed to work 10 years ago or so, but times were different then.
This is a fantastic newsletter. I have been a subscriber for a long time (previously Morning Cup of Coding), and I look forward to it every day.

It is such a convenient way to digest relevant information. Cannot recommend enough.
It's a sad place if you assume all the flaws in the article are obvious to everyone, then reduce everyones behavior to "orange man bad", and then complain about how it's a sad place.
As someone who regularly uses Powerpoint but isn't completely in love with it I don't see anything compelling on your home screen that makes me care about Pitch.

If there is some killer feature I don't know about it should be made more prominent. What I'm seeing is real time collaboration - which is already possible with Office 365 and some supposedly great templates. Switching software is a pain, so you better give me a good reason to.

It seems like you're squandering an opportunity to use Pitch to pitch me Pitch.
I had one thought forming while reading this piece, then read to Carmack's quote in the footnote which encapsulated it. I learned how to program modding games as a teenager, and as an adult now looking back on it, I realize how rough and ready the game engines were in 1996-1998, and how that rough and ready state, combined with my teenager's imbalance between time and money, led to a bunch of what Graham is calling early work where my bad 3d modeling skills, terrible art sense, and ability to sling values around in text files and use tools that other community members made, allowed me to make an entire faction for Total Annihilation that was clearly lower quality than the originals, but really not that much worse. Contrast that to about 2017 when I looked into what it would take to make a very small mod for XCOM, and boy oh boy, so much more work. What advantages I gained from being in that place at that time...
I wonder whether any service save witness protection or hitmen can achieve such wonders. Would be nice though.
I enforced the AGPL on my code, here's how it went (bad)
I too mourn the loss of the "interactive web" for want of a better phrase. Computer programs like Encarta used to be fun to explore and interact with. The same can be said of many '90s and '00s sites that would feature Easter eggs, or a unique method of navigation.

Bring any of this up today, and you'll immediately be met with a barrage of critiques about Flash security, or UX dogma like "Users prefer to scroll, not click around or hover on stuff."

The end result is the soulless, identikit web we have today, where the only things that display motion are the banner ads. We navigate through websites by scrolling alone, as though we were using a microfiche machine to read a newspaper from 1920.
> And which language do you have in mind when you imply that there are languages that are pronounced in the same way by all of its speakers?

That is not a requirement for updating the orthography or even the spelling. It also wasn't a requirement for introducing the writing system, print, etc. I doubt English has ever been pronounced the same way everywhere and likewise for any other language. Regional differences in spoken language did not stop e.g. Germany from updating its textual representation.

Funnily enough, your example looks perfectly readable to me. I'd guess it would be about as hard to read for English native speakers as Dutch is. It needs a few fixes (rivized -- only the first one should be an i, etc), but something like that would definitely be an improvement over current spelling.
This was previously submitted to HN 23 hours ago — and in fact, there's even a link to the previous submission at the bottom of the Matrix article, which is how I found it

https://news.ycombinator.com/item?id=24826951
How to Deploy a Next.js App to AWS ECS with HashiCorp Waypoint
Roasting coffee at home: in the oven. pan or skillet. popcorn popper
WRT needing to defend the mark: I was discussing what they seem to think is true, not necessarily that it was actually true, and that they are applying their interpretation fairly.

And legally required or not, publicly acting to defend the mark may put off others using something similar which is presumably the desire. A bit of a bully-boy tactic perhaps, but again I'm stating the fact rather than judging it.
Had a look at this 'securimage' and saw 'exploit' right away and this unfortunately put me right off if bots can bypass this alternative.

If a captcha is unable to do the job of keeping bots away even with 'better ux'. It is no better at securing anything than a wireless car key fob.
Just off the top of my head, I can see three parts that Amazon should be broken into: AWS, Amazon (the store) and AmazonBasics.
Wouldn't this make it even worse? It worked correctly, then they changed it to _not_ work for their sites?
streaming video?
OK. How about this:

"Meanwhile <any phone/mobile/internet/health-insurance provider> nothing"
Isn't this kind of tool doomed to suffer the "AI Effect"?

https://en.wikipedia.org/wiki/AI_effect

I feel like I use a ton of tools everyday that would have been considered "AI" 10 years ago, like content-aware fill in Photoshop, translation and correcting software, etc.
I might create a list like Google Font where you can preview all fonts for your Startup initials or search for a specific one. This should be a better UI than the current one I guess.
Wikipedia certainly does have animations and videos. Here's a list of literally every article with a video, there are over 5,000 of them at least:

https://en.wikipedia.org/wiki/Category:Articles_containing_v...

For comparison, Encarta had "over 300 videos".

And while it's not interactive, there are definitely animations on Wikipedia to help understand concepts, like the top of the article on pi shows a circle unrolling:

https://en.wikipedia.org/wiki/Pi

As for truly interactive explanations... I'm not sure there's really any kind of technological standard for that right now that people could collaboratively edit. At least not in the way JPEG and SVG are available to everyone. Do you have any suggestions?