zodiac

Does this require having a Rocq semantics of LLVM IR? Which one do you use?

In this case (the PHP bug), the "AI cycle" may have exposed the security vulnerability but it did not create it. If someone released a non-AI-based static analysis tool that was really good at exposing vulnerabilities I wouldn't expect that person to foot the bill of fixing the exposed vulnerabilities

Does snapshot/suspend/resume keep processes/RAM alive - or do you need to re-start processes/reload stuff into RAM? How does that work under the hood (CRIU?) and how fast is it?

We still care about computation and algorithms even when proving theorems in a classical setting!

For e.g., imagine I'm trying to prove the theorem "x divides 6 => x != 5". Of course, one way would be to develop some general lemma about non-divisibility, but a different hacky way might be to say "if x divides 6 then x ∈ {1, 2, 3, 6}, split into 4 cases, check that x != 5 holds in all cases". That first step requires an algorithm to go from a given number to its list of divisors, not just an existence proof that such a finite list exists.

No browser passes 100% of WPT, the leader is chrome which has about 1000 failing tests

1400 x $100,000 is $140 million, not $1.4 billion

Interesting, in this representation a plane is represented by the point on it closest to the origin, right?

I'm curious about graph algorithms that are "higher order" than what the article describes - e.g. how does Datalog encode the fact that two graphs (given as two relation sets) are isomorphic? How do I write a graph isomorphism algorithm in Datalog, or e.g. enumerate all graphs that have 6 vertices?

Something like "schedule a reminder to stop using the computer at 10pm so I can sleep by 11pm"? Since I want to sleep at 11pm local time every day

I think there’s syntactic ambiguity whether “faster” modifies “generates” or “code”