The caption on the close up says: “Details preserved on both face, face in the back in focus”. But it seems to me that a lot of detail is actually missing! On the later pictures you see a lot of skin “imperfections”, which looks much better. The 18 pro picture is way too smooth!
The reference implementation of BLAS is in Fortran, but these days fast implementations (using the same interface) tend not to be. OpenBLAS is in C and much of MKL is in C/C++. An individual widely-used package can be rewritten, much like improving a compiler, or giving it a new output, benefits lots of software all at once.
However, OpenBLAS still links to the reference LAPACK in Fortran, because it's mostly made fast by linking it to a good BLAS implementation. It could be rewritten, or converted to C with f2c. Although there's a long tail of useful but often niche Fortran software, some in Fortran 90 that f2c can't convert. Having a fortran compiler is still useful, and covers all of them at once. Potentially that compiler could compile to another language, to cover more and future platforms all at once (like f2c does). It looks like that's what's going on here, compiling fortran to wasm.
But if you program a for loop computing the sum from 1 to n, this also gets replaced by a constant (unless you build in debug mode). Why would an empty loop be different?
I think the argument is that the equivalent of an infinite loop would be a halt / abort instruction, not a complete removal of the loop and continue running anything else.
Not necessarily what you want in that case either: it's a common pattern in cases where you want the system to halt until you can attach a debugger to inspect the state. A halt/abort instruction that trashes that state would be undesirable (some CPUs have an instruction that is equivalent, but many do not, after all, why bother if you can just write an infinite do-nothing loop?).
A halt instruction is probably the appropriate representation for an infinite loop - the process gets stuck same as the infinite loop without proceeding. Abort is the instruction you want unreachable() to compile down into. It wasn’t an either or but both depending on the specific behavior you want.
Expecting a piece of code to be compiled to a precise sequence of machine instructions is exactly what you should not do with high-level languages like C++. Their task is exactly to abstract the machine away. They give you the guarantee that the final observable result will be what you asked for, not that the means to obtain that result will be what you have in mind.
If you write a loop to zero out some memory, it can be compiled to a loop, or to a call to an optimized predefined function, or even to a sequence of single zeroing instructions, if the size is small enough.
Even a single statement as a=0 may be compiled to a "load immediate" instruction, or an "XOR with itself", or a "sub with itself", or a move from another register known to be 0.
I'm not sure what this has to do with my comment. I am aware of all of this. It would be nice if an infinite loop was defined to be 'do nothing, indefinitely'. On architectures with an instruction that works that works precisely that way, it could be turned into that, perhaps, but that's an implementation detail and should follow the as-if principle (I'm also not sure any compiler would bother).
Sometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.
The recent proof of Fermats Last Theorem is interesting: it is (iirc) 13 million lines of lean code. And type-checking takes 5 hours or so on a pretty beefy machine. I cannot independently verify the proof, and I have to take Anthropics word for it that it actually type-checks.
That seems like a red herring. Have you independently verified the human generated proof of FLT? Surely someone else will try to verify Anthropic's formalization on different hardware. Plus, it seems likely that FLT formalizations will improve / get shorter over time, requiring less compute. And computers (and type-checkers) will continue to get faster over time as well. So maybe in 5 years you could own a computer fast enough to verify a/the proof in say a week, instead of 5 hours.
It'd cost you $30-$50 on AWS for a clean Lean build or maybe $100-$150 for the full verification suite. You are, in fact, capable of independently verifying the proof yourself if you don't trust all the people who've already done so.
reply