mdnahas

Agreed. Since sharing input between multiple applications (and the OS services) is its primary role, you would think that UI designers would have “thou shalt not steal focus” as a commandment, but that is not the case.

My latest version of the problem is with Ubuntu Gnome. Upgrade software and, later, you will be interrupted with a pop-up window to enter your system password. Not only is this an interruption, I’m always doubtful that this is the system asking for a sudoer password!

UIs, in my experience, are very bad at handling “interrupts”. Sorry, my dad designed chips, so I use that hardware term when talking about notifications and other times another application needs to notify or get the input from user. Personally, I’d have the UI change the color/texture of the system menubar/taskbar and wait for the user to click it.

For those that don’t know, the Quakers are like Zen Buddhism met radical Protestant Christians in the 1600s. There is no creed, no minister/priest/leader.

We sit together quietly for 60 minutes. If someone feels inspired, they stand up and speak. Then they sit down and the Meeting continues in silence. Some Meetings are silent from start to finish; others have speakers the whole time.

While there is no creed, people often speak about truth, equality, peace, and simplicity. I found it when looking for a belief system to pass on to my kids, should I have some.

If you’re curious, try it some Sunday. It’s an interesting experience.

They’ve done it twice now.

I’d argue in court that this is a pattern, not a one-off event and the damages need to be large enough to prevent this repeating.

Also, service providers are not identical. They chose Cloudflare because it was the “best” service. So damages include being moved to a worse service.

I’m the author of a tutorial on Rocq.

I’m surprised at the negativity on HN. We all want bug-free code and this is a way to not just reduce bugs, but eliminate whole classes of bugs.

Moreover, with proven code, we can have rock-solid libraries and code reuse.

Also, proven specifications allow LLMs to do divide-and-conquer when generating code. You can ask it to generate part A that does X, assuming part B will do Y. And then ask it to generate part B in parallel. And know that, when merged, the code will work.

And, provable code is good for LLMs because it will let LLM creators study hallucinations. The proof checker can identify what is a hallucination and what is not. This means LLMs may learn what they don’t know!

I’m not saying LLMs with proven code is nirvana. There are parts of systems where it doesn’t apply. Specifications are often complex and difficult to understand. Some important details are hard to write a spec for. And specs can miss things. But code proven correct by LLMs has potential to do real good.

Yes, you’re right, it is turtles all the way down. But, a huge part of the prover can be untrusted or proven correct by a smaller part of the prover! That leaves a small part that cannot prove itself correct. That is called the “kernel”.

Kernels are usually verified by humans. A good design can make them very small: 500 to 5000 lines of code. Systems designers brag about how small their kernels are!

The kernel could be proved correct by another system, which introduces another turtle below. Or the kernel can be reflected upwards and proved by the system itself. That is virtually putting the bottom turtle on top of a turtle higher in the stack. It will find some problems, but it still leaves the possibility that the kernel has a flaw that accepts bad proofs, including the kernel itself.

Also missing: Austin, TX

The banned websites have negatives, but they also have positives too. I hate to think of the young geeks banned from YouTube’s Kahn Academy, Veritasium, Smarter Everyday, …, and all the DIY tutorials.

An apt metaphor, … until I read recently on HN that storage on SSDs only last 1 year when unplugged.

https://news.ycombinator.com/item?id=46038099

I’ve used PocketBase in production. We ran into DB issues because the admin page loaded all orders and that climbed over 5000. I didn’t think that was much for a read-only operation, but when 5 staff were loading it every 30 seconds, it occasionally got very slow: 10 to 30 second load times.

Faster Vultr server didn’t help. The recommendation was to redesign the admin page to do search on the server rather than in the client. But that wasn’t possible at the time.

I enjoyed writing on top of PocketBase and running it. The developer was very helpful - quick, useful responses. My brother did his wedding website with it. It’s great for small projects. For higher performance ones, you will need to test and shift your design.

The announcement doesn’t say that they’re selling the Crucial brand. And it’s a valuable brand. So, I agree, they will wait for the bubble to pop and then start it back up. I assume the higher prices let them keep the operation around in mothballs and the employees working elsewhere in the company.

> None of those cities had problems with (insert stereotypical undesirable group) using public transit.

Austin. Tried it and rolled it back.

It was before my time here but I’ve heard: Homeless camped on the buses. Bored teens hung out on the buses riding nowhere and making trouble. Bus drivers demanded the change back.

I’m an economist and YIMBY activist. Only 10% to 15% of the Austin bus system budget comes from fares. (Most is a 1% sales tax.) I’d love to make the buses free. But it has negatives.

Anil, your blog is too wide for my iPhone 11 Pro’s screen. I have to scroll side-to-side to read it.

P.S. Half its value over 25 years is extremely stable if you look at the history of money, especially fiat money. It halved in value in 9 years, from 1974 to 1983.

Economist here. No, you don’t want that.

Inflation is annoying, but deflation is destructive. When that happens, people hold on to money as an investment and it doesn’t flow in the economy. The Great Depression was caused by deflation. (See Milton Friedman and Anna Schwartz’s A Monetary History of the US.)

As a result, central banks try to have a little inflation, so that random mistakes don’t push us into deflation. The Fed’s target is 2%. I think it should be a little higher. (See Fischer Black’s “Interest Rates as Options” and the shadow short-term rate.)

No one should be holding inflating dollars over the long term. That money should be invested in loans (bonds, mortgages, …) or equity (stocks, real estate, …). We have good ways of comparing investments over time by removing the inflation. These are CPI or the GDP deflator.

I went back to get an Econ masters and studied international currencies. Some exchange rates are very stable over time and we don’t know why.

Until you want to explain to your friend or elderly parent with a different phone how to use the app.

Here is the direct link to OpenSecret’s report on the Health sector. My blog post is out of date. Total lobbying is now $750,000,000. And that doesn’t count $420,000,000 in campaign spending.

https://www.opensecrets.org/industries/indus?cycle=2024&ind=...

If you want to know why the problem is hard to fix: healthcare companies spend $660,000,000 each year in lobbying. That’s more than $1,000,000 per member of Congress.

http://michaeldnahas.com/blog/numbers_that_matter/2019-9-15_...

We have done a lot to reduce risk, which has lowered the need for trust. We have national paper money, credit cards, insurance, flood-prevention infrastructure, FEMA (or did), etc.. We have less need for safety brought by connections with our neighbors.

And, with shipping being cheaper and the internet, you can stay at home and get food delivered, homegoods delivered, entertainment delivered, etc. and live without even interacting with your neighbors or seeing them at the local store.

Love Signal - Thanks!

Testing backups is important, separate of when you try to restore. It sucks hard to find out your backup is bad only when you go to need it. I highly recommend the quick, beautiful, and informative Tao of Backups.

Mike Nahas, Designer of Par2 file format

http://taobackup.com/

I’ve had a similar experience. I’ve edited Wikipedia pages for ages. I was able to create Wikipedia pages a while ago. Recently, I tried to create a page (“quantity controls”, a less well known relative of price controls in economics) and it got deleted for bullshit reasons.

I think that’s the key. When users pay, the company works to serve them better. When advertisers pay, the incentives are to attract users by any means (blinking lights, big emotions, fraud, etc.) and keep them on the website longer.

The latest example of this behavior for me is recipe websites that do SEO to get the top spot on Google and then serve you a 30-page long webpage full of ads with the recipe at the bottom.

I think a huge part of the world’s current problems come from “news” sites that are funded by ads.

Long bridges, like the Verrazano Narrows in New York City, have plans that account for Earth being a sphere. The towers at either end are not parallel, but tilted apart so that each is aligned with its local gravity.

Anecdote: I’ve run Linux and MacOS. I switched to Linux when Apple hardware got stupid expensive (soldered memory and harddrive) and Dell offered laptops with Linux installed. My brother was always saying “Apple just works … less hassle”. But he’s now worried about expense and privacy and moving to Linux.

I feel like the geeky bleeding edge is leaving Apple for Linux.

I read about this and started using binary search as my interview question. It worked well - about 2/3rds of highly credentialed applicants could not write a working implementation in 20 minutes. Most failures went into an infinite loop on simple cases! The ones who could write it usually did so quickly.

I think part of reason is that most people were taught a bad interface. Even the code on Wikipedia says “Set L to 0 and R to n-1”. That is, R is an inclusive bound. But we’ve learned that for most string algorithms, it is better when your upper bound is an exclusive bound, that is, n.

I’ve wanted to do an experiment testing that hypothesis. That is, ask a large number of people to write it with different function prototypes and initial calls and see how many buggy implementations I get with inclusive vs exclusive upperbound vs length.

The official newspaper of Russian Communists was also called Truth (Pravda).

https://en.m.wikipedia.org/wiki/Pravda

We don’t. We switch to proven-correct code. Languages like Lean, Coq, and Idris allow proofs of correctness for code. The LLM can generate proofs for most of the correctness conditions.

CI is still needed for performance, UI testing, etc. but it can have a much smaller role than it does now.

I was a quantitative trader for an options trading firm in the early 2010s. We were a very technical firms and hedges options trades within minutes. So, a trade with us would shift the stock price quickly. Even with that, we got scammed by traders doing this kind of thing on single stocks. My boss said that he complained to the broker and SEC, but nothing happened. We wrote code to limit our losses from this kind of scam.

We were probably able to find it because we did hedge quickly. Hedging costs money (trading fees, 1/2 spread) so some firms did it less often. We heard that Bear-Sterns only did it 1 time per day (around 4pm when spreads were small and over-night movement risk was nigh). They wouldn’t have caught this scam.

This sounds interesting. If you want to discuss it or just want a proofreader, please email me. I have done research in both distributed algorithms and economics. hackernews@mike.nahasmail.com

If you don’t know about these already, read about “self stabilizing algorithms”. They are fault-tolerant (to a certain definition) which is important in large distributed algorithms. I used one to build virtual networks with 10,000 nodes.

Location: Austin, Texas, USA Remote: only short jobs Willing to relocate: yes Technologies: economics, financial prediction (bonds, stocks, real estate), distributed algorithms, multi-threaded algorithms, linear algebra, formal proof, many languages (C,C++,Java,JavaScript,Coq,OCaML,…) Résumé/CV: https://www.linkedin.com/in/michael-nahas-1012232 Email: hackernews@mike.nahasmail.com

Designer of .par2 file format.

Successful quantitative trader (saved company $20k per day). Employee #7 for successful startup. Been analyzing real estate data for YIMBY non-profit.

I take hard problems and find the right math tools to tame them, then write the code to make it work in production.