japgolly

Interesting that they used both Lean and TLA+. I wish they'd speak more about that. I woulda thought they'd use one or the other. Generally speaking they both do the same thing (prove specs), but in very different ways.

That being said there was a story about him debugging an issue recently with some pretty serious help from AI.

But there's a rustfmt already. Anyway, the style guide is larger in scope than just code formatting.

Apply #[non_exhaustive] to publicly-exposed enums seems like a crazy recommendation to me. So much of the power of enums is that when you add a new case the compiler will flag all pattern matches that you need to update, which is a good thing because you're forced to consider each case. Having a catch-all saves dev-time but it risks not appropriately handling new cases becoming a runtime issue instead of a compile time error.

> Rather than storing all attributes in a single JSON column, we automatically extract the most frequently accessed attributes into separate, strongly typed columns.

I'm glad they made the discovery but this is DB 101

I assume the author is talking about `fold`, as in `[A] -> B -> ((B,A) -> B) -> B`, and not what I often think of as reduce as `[A] -> ((A,A) -> A) -> A`.

`fold` is awesome and super useful. It's the easiest and most convenient way to turn a collection into a single value. Put me anecdotally in the opposite bucket.

Nitpick for the author: it looks like you've got (a,b] when you actually mean [a,b). Either that or change the ≥ to be >.

Aren't AI's already G-rated cos of the built-in guardrails?

> every OS developer

They exempted Linux, from what I remember reading.

> Kunreisiki is also better for serious Japanese learners as it greatly simplifies the description of Japanese grammar: cf. matu/matte/matimasu (all with the same verb stem mat-) vs. Hepburn matsu/matte/machimasu (with 3 different verb stems)."

This is a silly argument because anyone learning Japanese is going to need to learn how to pronounce it anyway. Also "serious Japanese learners" would likely be using kana.

Detecting AI writing is a skill that not everyone has.

What does this even mean? In the future it will be considered too big?

> our hypodissipative result (which is not public), but as I understand it part of their training data

How did it become part of their training data if it wasn't public? /confused

They do have a cli: https://github.com/google-antigravity/antigravity-cli

Note: Anhedonia is the inability to feel pleasure or joy.

Ignoring the fact that their NAT was apparently wide open with no domain rules, a simple dashboard over their NAT showing requests grouped by domain could've gotten them a long way.

1) With formal verification you can prove properties about your system. With extensive testing you can also do the same but you need to take care and make sure you cover all possible cases.

2) With formal verification you can easily test things that are normally hard to cover by traditional testing. For example, if you want to test if that a postgres randomly goes offline, you don't lose any data, it's pretty hard to cover with extensive testing, whereas with formal verification you just say "postgres exists, it has state and can be online/offline, it can go online/offline at anytime" and you're covered.

In my opinion, it's not very different than writing an implementation of quicksort by looking at pseudocode in an algorithms book. You still need to write unit/property tests for your implementation if you want to verify it to be correct.

Any time you code up an externally specified algorithm, the onus is still on you to verify your implementation, even if the correctness of the algorithm is already verified.

Awesome read and absolutely loved the interactivity. A lot of effort was put into this.

KTLO = Keep The Lights On

> It’s time for AI to prove its unequivocal value to the world, and what better way to demonstrate that than to help finally cure diseases like cancer.

What a worthy goal!

The code doesn't work. I pasted in the full code at the end into Lean Web, and it gives 4 errors and a warning (all in the lemmas).

There's definitely less Scala jobs on the market these days.

It's about the feedback loop being so slow. Agents often compile and run tests to verify their work

Clicking on Scala results in a 404, same with Perl, same with Terraform

In 2013 I began work on ShipReq — an ambitious project to rethink how requirements are stored and maintained. Today I’m choosing to open-source this, my life’s work and magnum opus.

I hope someone somewhere enjoys this!

Scala is painfully slow to compile too

Good read here - https://www.luxdb.dev/architecture

This is amazing!! Super fast, I can actually enter symbols, search case-sensitively, I love it!

It takes orders of magnitude more effort to counteract bullshit than it does to produce it. Your opinion doesn't scale and not only is it easily exploitable by bad actors, it's happening in practice all over the place these days and is a huge, huge problem.