flaghacker

I'm not actually using formal verification at $DAYJOB, there we're using MILP solvers (which are closely related to SAT solvers) as part of the compilation flow when scheduling operations onto hardware accelerators.

I have been interested in formal verification for hardware for a while, but so far haven't found an opportunity to apply it. There are some great resources online though: the ZipCpu blog at https://zipcpu.com/formal/formal.html and SymbiYosys website at https://symbiyosys.readthedocs.io/en/latest/. I hindsight I could probably have used SymbiYosys instead of Z3, it would have saved me from having to walk the graph and map the gates to equations myself.

I also briefly wrote about my approach here, with less pictures but going into slightly more detail about how to convert circuits to z3 equations: https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079...

> The design should have been simple: if a session has been idle for more than an hour, we could reduce users’ cost of resuming that session by clearing old thinking sections. Since the request would be a cache miss anyway, we could prune unnecessary messages from the request to reduce the number of uncached tokens sent to the API. We’d then resume sending full reasoning history. To do this we used the clear_thinking_20251015 API header along with keep:1.

They clearly make the same distinction between the cache and the context. They're saying "we could reduce users’ cost of resuming that session by clearing old thinking sections". They intentionally created a behavior different between cached and uncached requests, specifically they clear thinking sections from the context for requests that miss the cache.

I'm asking as a non-webdev who never quite got what Redis actually does, but would love to learn.

The interpreter is slightly more clever and instead implements this as a copy-on-writr mechanism, but that's just an implementation detail .

A good resource for the "instead" case: https://unit8.com/resources/temporal-convolutional-networks-...

The "also" case is an example of 3D convolution, an example of a paper that uses it: https://www.cv-foundation.org/openaccess/content_iccv_2015/p...

1. From address 2. To address 3. bcc addresses 4. cc addresses 5. Time 6. Date

Is this really a reasonable request that the government is expected to answer? Doesn't this expose a bunch of private information about government employees and the people they interact with? I understand this post (and apparently the law) takes this as completely normal thing, but it seems really weird to me.

Some examples:

* exact times people are getting in/out the office (eg. the time in the morning when a person first answers an email from their boss)

* full information about holidays taken by all employees (eg. days/weeks during which no emails are sent)

* friendships or relationships (eg. any communication between employees that doesn't follow from the hierarchy or from team delineations)

* information from criminal investigations (eg. an investigator sending an email to the parking fine department probably means one of the cases they're working on is related to parking fines)

This all seems a huge privacy leak? Should this stuff even be called "metadata" if so much can be derived from it?

For even more proof, see "Figure 5: Space and time neurons in Llama-2 models" for single neurons in LLMs that already encode this information, without even having to use a probe model to extract it.

* The problem with large vectors is that they have large dot products with every other vector, which would imply that they are more similar to everything which doesn't make sense.

* Adding the requirement that "length==1" doesn't matter much in high-dimensional spaces, since that only removes one degree of freedom. Don't try to use too much 3D intuition here.

* It might be intuitive to think that "large" should have implications for the size of the vectors, but that really only applies to a couple of examples. We want vectors to represent thousands of unrelated concepts, so this one case is really not that relevant or important.

* In reality what ends up happening is partially the "very" dimension you're suggesting, but also just a "largeness" dimension. Individual dimensions can still have a scale!

As a historical note, Rust used to have green threads but they were abandoned a long time ago. This is a good talk about both the differences between different forms of concurrency/async and Rusts history with them: https://www.infoq.com/presentations/rust-2019/ (includes a transcript)

That may not actually be a problem though, since the current compiler executable is already good enough for almost any project.