lambda

I live in Vermont, where billboards are illegal. It's great, there is so much less visual pollution driving anywhere.

And yes, some people do try to push it, renting space to park their hay carts that happen to have their business information on the side.

But you know what? Those cases eventually get dealt with too, and overall, the law is a complete win, even with a few people testing the line.

> I suspect most experienced professionals start with the premise that the LLM is untrustworthy due to its nature.

Most people don't actually critically evaluate LLMs for what they are, and actually buy into the hype that it's a super-intelligence.

Would you be able to parse it in a streaming fashion and just store the structure of the document in memory, with just offsets for all of the string locations, and then re-read those from disk as needed?

With modern SSDs and disk cache, that's likely enough to be plenty performant without having to store the whole document in memory at once.

What Rust provides is a way to build safe abstractions over unsafe code.

Rust's type system (including ownership and borrowing, Sync/Send, etc), along with it's privacy features (allowing types to have private fields that can only be accessed by code in the module that defined them) allows you to create fully safe interfaces around code that uses unsafe; there is provably no combination of uses of the interface which lead to undefined behavior.

Now, yeah, it's possible to also use unsafe in Rust just for applying a local optimisation. And that has fewer benefits than a fully encapsulated safe interface, though is still easier to audit for potential UB than C.

So you're right that it's on a continuum, but the distinction between safe and unsafe code means you can more easily find the specific places where UB could occur, and the encapsulation and type system makes it possible to create safe abstractions over unsafe code.

There is no distinction between safe and unsafe code in C, so it's not possible to make that same distinction that you can in Rust.

And even if you try to provide some kind of safer abstraction, you're limited by the much more primitive type system, that can't distinguish between owned types, unique borrows, and shared borrows, nor can it distinguish thread safety properties.

So you're left to convention and documentation for that kind of information, but nothing checking that you're getting it right, making it easy to make mistakes. And even if you get it right at first, a refactor could change your invariants, and without a type system enforcing them, you never know until someone comes along with a fuzzer and figures out that they can pwn you

So, it's true that unsafe code can depend on preconditions that need to be upheld by safe code.

But using ordinary module encapsulation and private fields, you can scope the code that needs to uphold those preconditions to a particular module.

So the "trusted computing base" for the unsafe code can still be scoped and limited, allowing you to reduce the amount of code you need to audit and be particularly careful about for upholding safety guarantees.

Basically, when writing unsafe code, the actual unsafe operations are scoped to only the unsafe blocks, and they have preconditions that you need to scope to a particular module boundary to ensure that there's a limited amount of code that needs to be audited to ensure it upholds all of the safety invariants.

Ralf Jung has written a number of good papers and blog posts on this topic.

There's also "white" which is naturally occurring pure hydrogen.

Mostly it's seen as being economically infeasible to extract, though there is one working well in the world, and some other potential sources that may be feasible to extract discovered recently.

But the big problem with hydrogen is that right now, the majority of the supply is grey/brown/black, which all emit CO2 to produce. Green is far more expensive, and the carbon capture needed for blue is also expensive and the methods of storage are dodgy.

The thing about green hydrogen is that it's more efficient to transmit and store electricity than convert it to hydrogen and distribute and store that, so it's basically just a worse way of utilizing green energy sources. The only reason hydrogen is at all economical is that grey/brown/black are cheap, and it's hard to see any path for green or blue to become competitive (and truly zero emissions for blue).

It's possible that we'll find reserves of white hydrogen and efficient ways to extract it, but that's purely speculative right now, while building renewable energy sources, electric distribution, and batteries can be done right now.

I'm kind of puzzled by your first point. In my experience, parking apps require you to pay in larger chunks of hours than paying with coins used to; many times I have to pay for a minimum of 2 hours of parking with the app when I could pay for just 10 or 15 minutes of parking with coins.

DC fast chargers tend to cost much more than level 2 chargers. They have expensive equipment, more expensive electricity (intermittent high load is more expensive than more continuous lower levels, even for the same total power), and there tends to be a limited number of them so you want to encourage people to do level 2 charging when possible, and only DC fast charging on road trips when they really need it.

So prices are much higher than for normal AC charging. Most of the charging you do should be AC charging at your home or work.

This is complete FUD.

Even when charging on pure fossil fuels, generating in large plants with efficient turbines and delivering it to efficient electric motors is more efficient than pumping, refining, and delivering gasoline to millions of tiny piston engines.

But we don't charge on pure fossil fuels. The grid is increasingly powered by renewables and nuclear, which are less harmful to the environment than fossil fuels. Anthropogenic climate change could lead to mass catastrophe if we don't get it under control; it's already costing us billions and killing people worldwide.

And while our electric grid couldn't handle everyone switching to electric vehicles over night, the transition takes time, and we can invest in grid improvements as energy demand moves towards greater electric usage due vehicles.

You can also charge at work, which is actually generally better as the grid moves to more solar as then the demand lines up with generation.

Employers need to step up their game and start offering charging if they want people in the office.

The article mentions that it was provided by SciDev.net.

Looking there you find the original article, and it has the correction to the right temperature: https://www.scidev.net/global/supported-content/rwandan-scie...

The fire is still burning, is only partially contained, has gotten close to the Center, and the winds are forecast to pick up again tomorrow. So there's still a chance it will be at risk.

Now, they've had days to prepare for this, and apparently have plenty of contingencies in place, but this is still relevant the fire could get there.

I think you mean 2024 and 2023...

It's odd that it's .ru since the author is in Armenia.

This was being done over USB midi, which is already faster than standard DIN midi AFAIK. Trying to change the baud rate of DIN midi on both ends of the communication seems like a lot of work.

They have a library that allows you to write and verify formalized C code more easily. And they have actually written parsers for some common file formats in this, which have been used in some major projects; and that's good, because efficient parsers for complex file formats is one of the places where you really want to use C for its efficiency, but it's also really easy to make a mistake that leads to exploitable memory safety vulnerabilities.

Now that Rust is becoming more popular, it would be nice to be able to re-use these formally verified parsers in Rust, where your entire language is memory safe. The formally verified parsers can still be helpful, because the formal verification can ensure that you also won't crash (in safe Rust, you can still crash, you just won't be subject to arbitrary memory corruption).

But just using the C libraries from Rust is unsatisfactory, now you need to go through an unsafe interface which introduces a potential place to introduce new bugs. And there are existing C to Rust translators, but they generate unsafe Rust.

So this demonstrates a way to translate from C to safe Rust, though with constraints on the existing C code. It's both useful in that it means that you can translate some of these already formally verified libraries to safe Rust, and this research could be used as part of later work for a more general tool, that could potentially translate more C code to safe Rust while falling back to unsafe in cases that it can't reason about.

Anyhow, not all academic work like this ends up being used practically in the real world, but some of it can be, or some of it can be put into practice by other tools later on. Rust came about that way; much of its reason for existence is trying to put decades of academic research into a practical, real-world usable language, since there was lots of academic work that had never really been used in industry as much as it should be.

Except one of these incidents was a shoot down by Iran. So no, it's not just Russia, but Russia was responsible for two of the three incidents in question.

The example was talking about versions of another package that both of the given packages depend on. Not Python itself. The version numbers were made up.

You also need to consider that formal verification is not the be-all/end-all of correctness.

Formal verification is verifying a mathematical model of the program correct, according to certain mathematical correctness properties. That model may not actually represent the real world, or the correctness properties may not actually be the properties that you want to guarantee. Famously, there was the formally verified Java LinkedList implementation that was buggy due to the formal model not taking into account integer overflow.

There are parts of the Rust language and standard library that have been formally verified. That helps provide confidence that the basic model, of having safety properties upheld by unsafe core functions, to be sound.

But the big advantage of Rust, especially for everyday open source code that the world widely depends on, is that it strikes a good balance between a language that people actually want to use, and which can provide good practical safety guarantees.

Rust is far, far safer than C and C++. Most other memory-safe languages also are, but trade that off for lower performance, while Rust provides a similar level of performance as C and C++. And additionally, it's a language that people actually want to use for writing a lot of the core infrastructure.

As far as I know, I have never use any open source software written in Ada/SPARK. People just don't do it. The only reason they generally do is if they need to for functional safety reasons, in a high-criticality system, and they find it easier to get their software certified by writing it that way.

And even in safety critical systems, most people find using a subset of C, with restrictive rules, static checkers to check those, code review, and extensive testing, done by independent teams and testing on real hardware with requirements based tests that achieve 100% coverage at the MC/DC level is considered to be the gold standard of verification.

Formal verification can not possibly provide some of the safety guarantees that testing on real hardware based on actual system level requirements can provide.

Formal verification is one tool in a toolbox. It is useful for providing certain guarantees. But it's less important than many other factors for the actual improvements in safety that Rust can provide; by actually being used, in critical software that is exposed to potential network based exploitation, a memory-safe language like Rust makes a much better foundation than C or C++, and more people will actually use it in such a context than Ada/SPARK.

  the translated code may (quietly) not behave correctly.

The whole point of them show that example is that they say they catch this case, and bring it to the attention of the programmer:

  If the original C program further relies on x, our translation will error out, and will ask the
  programmer to fix their source code. This is another area where we adopt a “semi-active” approach
  to verification, and declare that some patterns are poor enough, even for C, that they ought to be
  touched up before the translation takes place.

That's true, but it's usually pretty simple to reverse engineer, and that's been done for a lot of cars. CAN message are generally sent out at fixed time intervals, and correspond to some physical or control value, with a simple linear mapping between some physical unit and the value in the message. You collect some CAN data, change something like pressing the accelerator, see what changes, record results.

Just search for "aftermarket ECU", you'll find lots of them; generally for high-performance cars that gearheads want to soup up further, but the same basic principle applies to most ECUs.

I think that was "versus replacing a chip."

The ECU has fairly standardized interfaces, mostly CAN or just simple switching circuits on or off. You can just get a replacement ECU. These replacement ECUs generally don't do things like using the O2 sensor to adjust the fueling, so they can burn dirtier than the original ECU.

Kyle Rittenhouse and Daniel Perry are both walking free after unambiguously murdering people in broad daylight.

You're right, I do find it less likely that the murderer of a CEO would get the same kind of treatment as murderers of civil rights protesters, but there are examples in recent history of people walking free despite unambiguously murdering people in broad daylight for political reasons.

I find that these efforts to make something that is almost but not quite JSON to be counterproductive.

It means that something you can't tell if it's JSON or another format. You'll have some tools that can work with it, while other tools will choke because they expect valid JSON. Oh, someone just switched the quoting style so now your jq based automation is all broken.

And now you have to figure out which of these not-quite-JSON formats this is. Is it HuJSON/JWCC? Is it JSON5? Does my editor have a mode that supports this particular variant, or am I always going to be fighting with it?

And finally, having used HuJSON for Tailscale config: the issue isn't just things like comments and trailing commas, or quoting styles. JSON is just a kind of heavyweight and cumbersome syntax for writing config files. I find that I prefer writing a script to auto-generate my Tailscale config, because editing it by hand is cumbersome.

There are a number of other possible config file formats, with varying levels of JSON data model compatibility. YAML has its issues, but we've all learned to live with them by now. TOML isn't bad, though good luck remembering the array of tables syntax. KDL is pretty nice; it has a slightly different data model than JSON, but it's actually one that is somewhat better suited for config files.

I'd rather use any of these for config files than something that is almost, but not quite, JSON.

That's one of the leading theories. Obviously, there's not enough information to say for sure.

But the CEO's wife has said that there were threats, possibly related to lack of coverage: https://www.cnn.com/2024/12/05/us/unitedhealthcare-ceo-kille...

> In an interview with NBC, Thompson’s widow, Paulette told the network that “there had been some threats” against her husband.

> “Basically, I don’t know, a lack of coverage? I don’t know details,” she said. “I just know that he said there were some people that had been threatening him.”

And the shooter wrote the words "deny", "defend", and "depose" on shell casings that were found at the scene: https://apnews.com/article/unitedhealthcare-ceo-shooting-del...

These words are reminiscent of the terms "delay, deny, defend", the title of a book about how the insurance company tries to avoid paying out on claims: https://en.wikipedia.org/wiki/Delay,_Deny,_Defend

So, one of the leading theories is that the shooter was motivated by some kind of case involving a denied claim. Obviously, there's not enough evidence yet to be sure of that, but that same frustration over insurers' failure to pay for necessary, life-saving treatments is part of why there's so much sympathy for the shooter and so little sympathy for the CEO who was shot.

Of course, there are also other competing theories out there; it's possible that the whole bullet casings thing is just a ruse to distract people. But anger about how health insurance companies rack in record profits by denying life-saving healthcare to people has become a large part of this story.

Yeah, I agree with you that there are larger problems that still need to be addressed; and that this stop isn't necessarily permanent, but something temporary that might come back once there are more controls in place.

But situations like this are nuanced and complex, and we are in a better position than we were a month ago, due to actions by the Biden administration.

It is easy, especially in cases of such long running problems like civil asset forfeiture, to get cynical and fall into the mentality that there's nothing that can be done. That's not the case. It is possible to improve things, through political and legal processes. Not always as easy as you would like. Frequently slower, and with regressions. But progress is possible, and it's worth keeping track of who makes that progress to inform future voting patterns.

Cynicism can be an effective tool to blunt efforts at reform.

That was an example to illustrate how little basis they needed for these searches in previous cases, not intended to be a guess for what the reason the person at the start of this thread was stopped.

The point is, this whole "cold consensual search" policy was based on nothing other than the officer's personal opinion for who should be approached and searched; because it was theoretically "consensual", they didn't need any kind of basis for making the determination.

The order to stop the program of "consensual searches" at mass transportation facilities was sent out on November 12, and the more detailed report that I linked to on November 21st. Do you have knowledge of these DEA consensual searches happening at airports or other mass transit hubs after November 12?

Or are you referring to broader law enforcement attempts to do consensual searches or civil asset forfeiture seizures, which are absolutely still a problem?

I guess my point is, there are still massive problems with the way policing happens in this country. But the Biden administration has ordered this particular problematic behavior to end, specifically in response to the incident brought up in this article.

So, are you just making vague generalizations, or do you have actual knowledge that this program has not ended?

When someone responds like this, it's not to specific features, but to the general over-saturation of "AI" features because they are trendy, despite the majority of such features being poorly thought out, misleading, poorly integrated, provide serious privacy concerns, don't address concerns about bias or hallucination, etc.

If the marketing copy actually referred to specific features, rather than the "AI" buzzword of the day, people might be less likely to interpret it as a negative signal.