MurphyA/hacker-news huggingface dataset:
by pron | 2025-07-31 10:23:59+00:00
But both Dafny and Lean (which are really hard to put in the same category [1]) are used even less than TLA+, and the problem of formally tying a spec to code exists only when you specify at a level that's much higher than the code, which is what you want most of the time because that's where you get the most bang for you buck. It's a little like saying that the resistance to blueprints is that a rolled blueprint makes a poor hammer.

TLA+ is for when you have a 1MLOC database written in Java or a 100KLOC GC written in C++ and you want to make sure your design doesn't lead to lost data or to memory corruption/leak (or for some easier things, too). You certainly can't do that with Dafny, and while I guess you could do it in Lean (if you're masochistic and have months to spare), it wouldn't be in a way that's verifiably tied to the code.

There is no tool that actually formally ties spec to code in any affordable way and at real software scale, and I think the reason people say they want what doesn't exist is precisely because they want to avoid the thinking that they'll have to do eventually anyway.

[1]: Lean and TLA+ are sort-of similar, but Dafny is something else altogether.
by twhitmore | 2025-07-31 10:25:31+00:00
Checked exceptions were a reasonable idea, but the Java library implementation & use of these was totally wrong.

Checked exceptions work well for occasional major "expectable" failures -- opening a file, making a network connection.

They work extremely poorly when required for ongoing access or use of IO/ network resources, since this forces failures which are rare & impossible to usefully recover from to be explicitly declared/ caught/ rethrown with great verbosity and negative value added.

All non-trivial software is composition, so the idea of calling code "recovering" from a failure is at odds with encapsulation. What we end up with is business logic which can fail anywhere, can't recover anything, yet all middle layers -- not just the outer transaction boundary -- are forced to catch or declare these exceptions.

Requiring these "technical exceptions" to be pervasively handled is thus not just substantially invalid & pointless, but actually leads to serious rates of faulty error-handling. Measured experience in at least a couple of large codebases is that about 5-10% of catch clauses have fucked implementations either losing the cause or (worse) continue execution with null or erroneous results.

https://literatejava.com/exceptions/checked-exceptions-javas...
by MrSkelter | 2025-07-31 10:25:36+00:00
This was all widely reported. The problem here is that people don’t read and they routinely dismiss stories based on source, not content.

The 9/11 attacks were incredibly bizarre from day one. Everyone with any knowledge of the world immediately started asking questions.

Also remember that the attacks were the largest terrorist incidents by death for non-American countries. NY is a world city. More British people died that day than in any other single terrorist event - and that’s a country dealing with the IRA. That meant immediate global press and government investigation.
by bonoboTP | 2025-07-31 10:25:54+00:00
Once I felt like I'll be really attentive and answer confidently, and in the end I got overminused. The hesitation is part of the signal. If it's 1% sharper, even if you can tell which one is 1% sharper, you gotta say hmmm number 1 is a bit better but just a little.

Adding -0.5 to the diopter will often make the distance noticeably sharper in appearance while not really giving you more lines you can read, it's a sensation of sharpness but not really more info. And for that you a price because near vision will require straining your eye muscles to accommodate, and that will often cause headaches and tiredness after reading or working at a monitor.
by bartread | 2025-07-31 10:27:04+00:00
It's 100% this. Anyone who's run a website or web app for any length of time in recent years and makes a habit of inspecting their logs will quickly realise that they're being scanned by bots looking for vulnerabilities multiple, or even many, times per day. The search for vulnerabilities is entirely automated and will pick up any domain that has a website or web app attached to it.

One those vulnerabilities are found, the hackers will pounce, and, whilst ransomware is one potential outcome, they might instead do all of the kinds of things GP has described. They don't care what the site is for or what industry you're in.
by turkishmonky | 2025-07-31 10:27:55+00:00
I have this workflow with the ytdl-sub docker on my k8 cluster, is pretty powerful at filtering to specific videos and includes sponsorblock - everything is configuration driven, no ui, which can just be dropped into a yaml configmap

I rarely have to touch it unless I'm adding a new playlist or channel

https://ytdl-sub.readthedocs.io/en/latest/introduction.html

It's been great, the kid can watch any channels on there she wants on her ipad with no ads or sponsored segments
by RossBencina | 2025-07-31 10:28:06+00:00
Lean does not reduce the mathematical search space as you suggest. Yes there is a fixed, compact low-level logical core that everything above it depends on. But this is equivalent to an encoding of the logical foundations that mathematics, that formal mathematics depends on in any case. On top that you have mathematical theories built on assumptions (axioms) and you can specify whatever axioms you like and change them at will. To use your analogy: the "search space" is parameterised by user-defined sets of axioms and assumptions.
by otikik | 2025-07-31 10:28:55+00:00
I think "junior programmer" (or "copilot") oversells the AI in some cases and undersells it in others. It does forget things that a regular person wouldn't, and it does very basic coding mistakes sometimes. At the same time it's better than me at some things (getting off-by-one errors when dealing with algorithms that work on arrays). It also has encyclopedic knowledge about basically anything out there on the internet. Red-black Trees? Sure thing. ECS systems for game programming? No problemo, here are the most used libraries.

I have ended up thinking about it as a "hunting dog". It can do some things better than me. It can get into tiny crevasses and bushes. It doesn't mind getting wet or dirty. It will smell the prey better than me.

But I should make the kill. And I should be leading the hunt, not the other way around.
by palata | 2025-07-31 10:30:09+00:00
To echo the article, I don't want to know it was written with an AI. Just like I don't want to see that it was obviously copy-pasted from StackOverflow.

The developer can do whatever they want, but at the end, what I review is their code. If that code is bad, it is the developer's responsibility. No amount of "the agent did it" matters to me. If the code written by the agent requires heavy refactoring, then the developer has to do it, period.
by jerieljan | 2025-07-31 10:30:56+00:00
The trick to this is to run a LiteLLM proxy that has all the connections to whatever you need to connect to and then point Open-WebUI to that.

I've been using this setup for several months now (over a year?) and it's very effective.

The proxy also benefits pretty much any other application you have that recognizes an OpenAI-compatible API. (Or even if it doesn't)
by aurareturn | 2025-07-31 10:31:00+00:00
"He made a reference to billionaires, okay?" Scott said of Hawley. "I don't know when in this country it became a negative to make money. But somehow, if you've made money, you're supposedly — I think Senator Hawley suggests — you shouldn't be serving, because you might trade stocks." "Anybody want to be poor? I don't." Scott continued. "Right? So this idea that we're going to attack people because they make money is wrong. Is absolutely wrong. We should cherish all of our different backgrounds. ... So, I think it's disgusting what is going on here."

This is Republican Sen. Rick Scott by the way.

Seems like he's using some form ad hominem to distract from the actual purpose. The purpose is not to prevent congress from getting rich. The purpose is to remove conflict of interest. Congress can have insider info on individual stocks. For example, knowing that Oracle will get approval to buy Tiktok early can change Oracle's stock price. That's insider info.

I think only allowing congress members to buy and sell index funds is fine. Not individual stocks. Or if they want to trade individual stocks, make them declare 1 month earlier and make it public.
My Journey to Pure No-Code Addition (Spoiler: Plot Twist Ending)
by tibastral2 | 2025-07-31 10:31:16+00:00
TL;DR: Spent 6 months trying to build addition in "no-code". Ended up writing pure functions. I am now enlightened.

Month 1: The Dream

"Code is gatekeeping! I'll revolutionize math with pure visual programming!"

Buys 7 no-code courses, $2,400 in SaaS subscriptions

Month 2: The Workarounds

- Tried pre-built text elements (2,500 combinations, Bubble crashed)

- Attempted human-in-the-loop via Zapier + email (grandmother got tired after 50 calculations)

- Explored blockchain oracle services (gas fees: $12 per addition)

Month 3: The Bargaining

"Maybe just tiny bit of logic?"

- IF/THEN workflows (wait, that's Boolean logic)

- Mathematical operators in Bubble (wait, that's... math code)

- Excel formulas (DEFINITELY code)

Month 4: The Acceptance

Discovered that addition is... computational. Who knew?

Month 5: The Revelation

Every "visual" operation was just:

- Model (data structure)

- Update (state transformation)

- View (presentation)

The Bubble "visual workflow" was trying to be The Elm Architecture!

Month 6: The Awakening Opened a text editor. Typed in elm:

add : Int -> Int -> Int

add a b =

a + b

-- Or even better:

add = (+)

Runtime: 0.001ms

Cost: $0

Dependencies: 0

Side effects: None (guaranteed by compiler)

Bugs: Impossible (thanks Elm!)

I am no longer no-code. I am pure functional. I have discovered mathematical truth.

Posted from Elm reactor (my Bubble subscription has been cancelled)

Update: Learning that functional programming is just applied mathematics. Turns out mathematicians invented the ultimate "no-code" 300 years ago - they called it "functions". Who's gatekeeping who?

P.S.: My addition function is now proven correct by the type system. Beat that, drag-and-drop!
by apabepa | 2025-07-31 10:31:43+00:00
For me it is difficult to give good code comments just when code is written. The problem is solved, the tricky parts if any are internalized. I dont mind reading code so just documenting what the code is doing does seldom bring value. The important thing is to document why the code does things in an non obvious way and unintuitive scenarios and edge cases etc.

When revisiting code is the best time to add comments because then you will find out what is tricky and what is obvious.

Code reviews are also good for adding code comments. If the people reviewing are doing their job and are actually trying to understand the code then it is a good time to get feedback where to add comments.
by sevensor | 2025-07-31 10:33:52+00:00
RFC 8259 is a good read and I wish more people would make the effort. I really don’t mean to bash JSON here. It was a great idea and it continues to be a great idea, especially if you are using javascript. However, the passage you quote illustrates the same shortcoming I’m complaining about: RFC 8259 basically says “valid primitive types in json are the valid primitive types in your programming language,” but this results in implementations like Python’s json library emitting invalid tokens like bare NaN, which can cause decoders to choke.

I think what JSON gets right is that it gives us a universal way of expressing structure: arrays and objects map onto basic notions of sequence and association that are useful in many contexts and can be represented in a variety of ways by programming languages. My ideal data interchange format would stop there and let the user decide what to do with the value text after the structure has been decoded.
by rcxdude | 2025-07-31 10:35:44+00:00
Difficult to do over any significant range: gravity drops off with 1/r^2, gravity gradient like what they seem to be using here (easier to measure while in motion) drops off with 1/r^3. The variations in the earth are due to fairly large density variations in massive sections of the crust, and a ship and especially an aircraft is absolutely miniscule in comparison, even if the density contrast is higher.
by stingraycharles | 2025-07-31 10:35:59+00:00
Yeah I don’t understand this problem, who uses so many agents at the same time in the first place?

And if this is really a problem, why not funnel your AI agents through a proxy server which they all support instead of this hacky approach? It would be super easy to build a proxy server that keeps track of costs per day/session and just returns errors once you hit a limit.
by potato3732842 | 2025-07-31 10:36:33+00:00
>who no one else really cares about, and he's invoking some grand criticism of government writ large as a way of bringing urgency and grandeur his idiosyncratic interest that doesn't really matter in the grand scheme of things.

Everyone with a pet interest levies just about the same criticism at government and it paints a pretty consistent picture.

Whether you wanna develop EV chargers, buy discounted office space and turn it into residential, open a coffee shop, etc, etc, the same stupid government red tape born at the behest of generations of stupid voters who couldn't think a step ahead or about the big picture stand in your way.

>I'm generally in favor of deregulation or deregulation, but I generally feel <bunch of text>

Sounds like "believe in deregulation" only to the extent that you can lie to yourself and say that you do. You really believe in high regulation, but deep down you know that's a bad thing to believe in so you reframe it so you can sleep at night. You are a worse person than one who believes in regulation and is honest with themselves about the tradeoffs of it and has made some assessment that it is still worth it.

If you wanna prevent bad outcomes then make people liable for bad outcomes. The current status quo where all the cost of litigating a bad outcome must be born by every single party up front in the form of surveys, studies, impact assessments, etc, etc, steals money from literally all of us in one way or another, puts some in the pocket of government and puts orders of magnitude more in the pockets of well positioned private parties who government essentially makes work for is beyond insane and anyone who supports it is of bad character.
by defrost | 2025-07-31 10:37:03+00:00
If you happen to run three clusters of mag sensors (X,Y,Z on each wing tip and another group of three on a tail boom) then you are measuring a differential field against three points for each axis and sensing the induced ground change from a diurnally fluctuating field .. also getting different results depending on whether you are traveling North to South, East to West, or at some other angle.

Despite all that, maps are still produced of the leveled and normalized ground field (see geomagnetic maps).

Using the geomagnetic as an assist / backup to navigation reduces to something similar to the use of a DTM as an assist - not much use in flat areas, useful in areas with distinct features, easily confused if one valley looks much like another.

The daily flux is an issue, of course, but your software, hypothetically, would be looking at the preserved shape of waves on the ocean despite the fact that the tide is rising and falling all around.
by riedel | 2025-07-31 10:37:53+00:00
> Speaking of ADHD, sometimes I wonder whether that might be a false positive self-diagnosis in my case. > > About 10 years ago, when I consumed much less media content like Instagram or YouTube, everything was different in that I used to be an avid reader of fiction, which I now can hardly do without losing focus.

I have recently at the age of 45 went through the trouble of getting myself 'diagnosed'. The whole process and theory is IMHO all very hand-wavy. I guess it boils down to the fact, if one's neurotype is incompatible with one's life you can call it illness and you need to give it a name to get treatment/help. In my case I don't want to take drugs, however, I am more self aware, which helps a bit creating less damage to myself and others (hopefully). It helps a bit also giving it a name myself and looking for better tools. While I certainly had trouble in my youth (which mostly my mother covered for me), it wasn't that much of a trouble in between, but as I grow older m ability to compensate by staying up all night to wait for some focus is decreasing. Regarding distractions: for me it is rather HN than YT, because it keeps my brain busy without pushing too much trash and ads into it as a side effect.
by RossBencina | 2025-07-31 10:37:57+00:00
> Is there a way to read lean proofs noninteractively.

I'd like to see an answer to this question. I was looking into it the other day.

I found this: https://xenaproject.wordpress.com/2019/02/11/lean-in-latex/ Which gives a way to do the clicking-through outside the editor. And maybe gives some insight into how Lean people see things.
by GreenWatermelon | 2025-07-31 10:38:25+00:00
I think "natural" here would refer to genuine project rrquirequirements that will translte directly to value to customers e.g. customers demand x features in y time and we don't have enough manpower to handle it. This is natural, it's business survival.

Contrast with the Unnatural cause of "manager just wants a promotion at any cost" which, in a sense, is akin to Embezzlement. The manager worsens business prospects and contributes to organizational rot for their personal gain.
by robocat | 2025-07-31 10:38:57+00:00
> "To put this into context, the scam center industry in Cambodia is estimated to generate over $12.5 billion annually – in other words, around half the country's GDP,"

Commercialisation of criminal activity is a massive growth industry.

I'm unsure how high-trust societies will be able to defend against invisible puppet-masters finding local defectors that will (a) rip off locals, (b) be the scapegoat.

My friend woke up the other day to someone grinding to steal copper. Defectors don't need expensive payoffs - just a few dollars (and are best paid illegally e.g. Meth anonymously via gangs?).

Perfect a scam in country A, then deploy it to country B (say New Zealand which relies on high-trust cooperator good citizens to function, and where the majority of people have no immunity against criminals - trust is a learnt behaviour here and many people can't detect the untrustworthy).
by jve | 2025-07-31 10:39:30+00:00
> The risks of vendor lock-in, losing control of your files

As for Figma, being able to export SVG is lock in really a concern here? Many tools support .svg. So to me lock-in ain't even a concern for a tool like figma.

And you noted it well - I seem not to care if it is a web app if it works well: Figma, VSCode (Performance as a feature)
by adrian_b | 2025-07-31 10:39:35+00:00
The applications of BPS are entirely different.

BPS depends on terrestrial stations instead of satellites, like Loran, which was used in the past.

BPS is at least as easily jammed or disabled as GPS.

With the gravimeter discussed in the article, and with adequate maps, one can navigate autonomously, without depending on any external help.

Moreover, BPS appears to be intended to cover only continental USA. There are no plans to use radio frequencies that would allow global coverage, like Loran had in the past.
by flanked-evergl | 2025-07-31 10:39:45+00:00
I'm somewhat opposed to the idea of having a walled garden App Store as Apple does, which is why I don't use Apple.

But Apple insists they do have a walled garden, and people buy Apple with that expectation, so I certainly hope and expect that Apple doesn't approve apps like these. Any app that does doxxing as a service should not be on Apple's app store IMO.
by MaxBarraclough | 2025-07-31 10:40:35+00:00
> that is why i said it depends and put "proving" within quotes

I feel I need to insist on this point: a design-by-contract methodology using runtime checking may be an effective means of improving software quality, but it certainly isn't proving the correctness of a program. Using the word 'prove' here is just plain wrong. Putting it in quotation marks doesn't help. It simply does not constitute a proof.

> It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject

I'm not insisting on a narrow understanding of formal methods, I'm insisting on proper use of established terminology.

I'm all for practical methodologies that benefit software quality without paying the enormous costs of fully applying formal methods. Design-by-contract with runtime checking seems like a reasonable approach. (Static typing is another. Effect-oriented programming might be another.) My point was just about the proper use of the word proof.

> Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools.

A program is proven correct only when the proof is absolute, which implies fine-grained. I'm not opposed to the use of partial proofs or 'good enough' proof-sketches, both of which could be useful in producing high-quality software in the real world, but we should be clear in how we refer to them.

I'm not sure about the idea of proving correctness by hand, though. Manually applying a formal model of a real programming language sounds unworkable. If code is well structured, it should be possible for the programmer to reason about it somewhat precisely, like a proof-sketch, but that's not a proof of correctness.

> The Programmer plays the role of "theorem prover" when using DbC

I don't find this convincing. There's nothing stopping the programmer from failing to notice some error. If you aren't actually doing a proof, just say so. There is no stand-in.

> tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs.

Right, I hinted at this in my previous comment. SPARK Ada does this. In that case, correctness properties of the program are indeed formally proven. That's a quite different methodology to design-by-contract with runtime checking though, to the point that it almost seems unhelpful to refer to them both by the same name. I've had to be careful to explicitly state design-by-contract using runtime checking this whole time.

The deeper distinction here is between testing and formal proof, and design-by-contract can in principle refer to either.

> here is a case study Design by contract formal verification for automotive embedded software robustness

Have only skim-read but seems somewhat similar to this case-study about SPARK: https://www.adacore.com/tokeneer
by theandrewbailey | 2025-07-31 10:41:39+00:00
I usually load my blog to check internet connectivity.

I work at an e-waste recycling company. Earlier this week, I had to test a bunch of laptop docking stations, so I kept force refreshing my blog to see if the Ethernet port worked. Thing is, it loads so fast, I kept the dev tools open to see if it actually refreshed.
by diggan | 2025-07-31 10:42:41+00:00
> Ollama is set on becoming the standard interface for companies to deploy "open" models.

That's not what I've been seeing, but obviously my perspective (as anyone's) is limited. What I'm seeing is deployments of vLLM, SGLang, llama.cpp or even HuggingFace's Transformers with their own wrapper, at least for inference with open weight models. Somehow, the only place where I come across recommendations for running Ollama was on HN and before on r/LocalLlama but not even there as of late. The people who used to run Ollama for local inference (+ OpenWebUI) now seem to mostly be running LM Studio, myself included too.