wbeckler

I think the royal combo is Lean 4/TLA+/etc. plus AI plus a deterministic generator. For large systems formal method assertions need to be compressed down to a human comprehensible size. This can happen when the assertions are confirming the accuracy of a model and its attached code generators. The generator can generate proofs of the generated code and a human only needs to ensure that the generator provably generates the correct mass scale assertions.

This is how formal methods can constrain AI for large systems.

We're doing this at the Open Markets Initiative, where we've generated millions of lines of Lean 4, TLA+, and Rocq that ensure that our open source electronic trading protocol code is accurate. We didn't expect it but the Lean prover did identify some incorrect steps. https://github.com/Open-Markets-Initiative

Proof that nonfiction is wilder than fiction.

Here's the article in Germany about the incident: https://www.rtl.de/news/russische-spionage-rtl-reporter-unde...

The article didn't describe how the second AI is tuned to distrust input and scan it for "disregard that." Instead it showed an architecture where a second AI accepts input from a naively implemented firewall AI that isn't scanning for "disregard that"

Here's a list of global locations: https://livecode.nyc/network

I hope that pun is intentional.

What's the threat scenario where forcing a password reset increases security? I'm genuinely curious, because I feel it's often the case that password expirations might introduce more threats than they mitigate.

It looks like it already failed: https://www.reddit.com/r/BalticSSRs/comments/1dpbto6/bolivia...

https://x.com/upholdreality/status/1806090907084865627

I've heard great things about Vega [1], which sits on top of D3. It's a dependency of OpenSearch Dashboards, allowing users to create custom dashboards on log and observability data [2]. The vega library might alleviate some of the concerns others are expressing about the learnability of D3.

[1] https://vega.github.io/vega/docs/ [2] https://opensearch.org/docs/latest/dashboards/visualize/vega...

60 years ago

I love your animations! How did you do those?

I hate when writers describe plants as an ongoing carbon sink. They are a one-time carbon sink. So using "cars" as a comparison to carbon volumes is confusing, because cars will keep emitting after a plant is full grown and starts shedding leaves and wood that turn back into methane or carbon dioxide.

The key benefit of the plants is cooling the city without electricity, which is an ongoing effect.

The typical temperature chart is an average across the planet or a region. Definitely not population-weighted.

Are you saying that the prevalence of trees among good-performing solutions is not related to superior performance of trees over other architectures, but rather that more people are trying them out and they will show up in the winning solutions more often because of the implementation rate?

It could be related to the fact that they didn't have much space for a normal size tailhook, as stated in the article.

You're assuming there was no need-based tuition program already running. Average tuition may not be full tuition.

I see lots of criticism of tactics in these comments, but isn't the proof in the pudding? This was a wildly successful campaign that will have a significant positive effect on many people's lives while also reducing emissions. It's a win-win-win. This seems to me proof that blocking traffic, vandalizing museums, and all the other seemingly "nonsensical" tactics are in fact the right move at the moment.

I feel like the MacBook is the elephant in the room here

Does Keep have an open core business model, where they host your stuff using a proprietary control plane for a fee and introduce proprietary features around the edges?

I feel like these concepts don't go well together in a single list. There's a big leap from "using logic" to using repetition, e.g., "of the people, by the people, for the people."

I think a good question might be, what language is better for gpt to program. If you want to write applications that accomplish intelligent things via symbolic manipulation, is lisp a good language to ask an AIto write it in? Is PAIP in the learning set for GPT4?

If the issue was the prompt, I expect someone will prompt it with a better wording of the problem and get a decent algorithm, and post it in this conversation. Let's see what happens...

I've lived in the UK and the US. The taxes are about the same.

There's a framework to do this in most major languages. I think python started this with TestDoc.

Kenji's 3-ingredient mac and cheese is a masterpiece. It's become the go-to meal for my kids. It also has to be the peak in energy efficiency for pasta.

The idea is that by minimizing the water you can maximize the starchiness of the water, which creates a great emulsifier for the cheese sauce, along with evaporated milk. The combo is truly creamy mac and cheese, with no grittiness or separation of oils. It tastes great, it's faster than Kraft, it's energy efficient, it's easy to learn (literally 3 ingredients plus water).

It also has easy-to remember-units (6 oz pasta, 6 oz cheese, 6 fl oz evap milk). The evap milk amount perfectly divides the USA standard 12 fl oz evap milk can.

Kenji has tweaked the ergonomics of scratch mac and cheese light years ahead of where it was.

Google "mysql booking.com" for a beast of an example. There's lots of content out there about that one.

Did you know that OpenSearch has JDBC/ODBC drivers? https://github.com/opensearch-project/sql

I worked in this field and I am certain this is an urban legend. Do you know of any evidence of this "well known" phenomenon?

Maybe the I/O pattern could be hideable using confidential computing, like with a Nitro Enclave.

The Schrems II ruling was that DPA+SCCs are insufficient for transferring data to a US company. You need to have "supplementary measures" in addition to the SCCs.