Why must they do worse?

To me it would seem for generating proofs LLMs would be much better at guessing than simply blindly breadth-first-search would be, with any manually-written heuristic.

Indeed I expect large parts of proofs would be applying existing patterns and LLMs would be good for applying structures they've been trained on. In particular generating the required tons of training material should be pretty straight-forward.

Such a model could then be a proof strategy in Rocq (previously known as Coq).

Good thing verifying formal proofs is basically mechanical work and the tools to do it automatically exist already.

Just in case you were lamenting that it's not written in Rust, fret no more, you can find one at https://ancillary-proxy.atarimworker.io?url=https%3A%2F%2Fgithub.com%2Fsouk4711%2Fha...

I wasn't able to make hakoniwas file-based restrictions to work, though. Complains about "fully incompatible access-rights". And its cli tool documentation is worse. Overall it seems the tool linked here is better.

It would have been so much nicer to mess up with the results to subvert the operation.

Perhaps it would have been too big of a business risk, though. Maybe they could've brought CIA along, or just blamed them anyway.

If you've followed the story, they person opposing this was not *forced* to integrate anything, as the code was not going inside his subtree.

Nevertheless, he was opposing in principle the existence of shared Rust DMA interfacing code. Instead, each Rust driver should use their own interfacing.

The maintainers can quit for whichever reason (or no reason at all), but if they do, in this case it's not probably a good reason.

IRC iss closed federation: you need to agree with the network admins to get your server linked. In addition, the servers are manually configured to conform to a tree structure network, not free-form one.

I believe nowadays the term federation by default means open federation.

Well, let's just agree to disagree.

Whether you like it or not, it seems quite certain to me that most code is written in ten years is going to be written with the help of of an AI assistant, LLM or some new approach.

It's just that useful.

With the help of safe frameworks and safe languages reviewing most of the code you'd generate with an LLM is pretty straight-forward to review to be safe.

LLMs are a useful tool when you don't know the answerâ"or can't be bothered to come up with itâ"but it's easy to verify if the results are correct.

Such is the case with e.g. programming.

Thanks, this seems quite useful!

Connecting over ssh can take a bit of time, e.g. if I want to list all connected clients in all APs. This is quite possibly faster than using ssh to do it.

If you have a VLAN-able switch, you can use one port for all the traffic. 2.5G should be fine for 1G uplink, and most people have less.

But yeah, it's mostly a WiFi router. I wouldn't expect to see WiFi hardware on a "real" router.

Luci is a web user interface for people, not an API for computers.

As far as I know, OpenWRT doesn't really provide an API outside localhost, and then that API is basically Linux. I think having a REST API would be quite nice.

Even if they were audited, are they formally verified? Probably not. Are the C library function they may end up calling in many cases formally verified? Most certainly not. Though, you could be using CompCert for compiling them, but it doesn't stop you from compiling garbage.

Audition isn't a silver bulletâ"and actually formal verification isn't either, if you are verifying the wrong thing. But the bar for formal verification is a very high and the results increase the trustworthiness of the code by a lot.

Good to know. I've do write Rust but never considered that. From the (safe) programmer's point of view that's invisible, so Rust is permitted to do that.

Alignment boundaries-based field reordering is a good feature, but how about dealing with false sharing? It would be very wasteful to align everything by cache line size and you can't know from the struct definition itself how they should be ordered best.

You'd use #[repr(C)] or a crate like PacketStruct to deal with that.