fsmv

Computable includes BPP

But how will you know that the query plan actually does what your query asked for?

I think there were some who really cared but I also think a lot of the 4chan types that found him egged him on and tried to trigger his schizophrenia because they treated it like it was all a big joke.

It really is tragic. He deserved better. RIP King Terry https://youtu.be/Xb9GBLPCeVw

But what does it mean? The theorems are just symbols in lean. The conjectures humans chose are carefully selected to be the questions that are interesting and relevant to our intuition about the real world.

Math often doesn't have applications for hundreds of years and that application is only possible because people deeply understand it and how it applies to the real world.

Generating an endless list of true statements doesn't really do anything, those things are already true regardless of whether someone has written a lean program to model them.

The entire point of writing proofs is for advancing human understanding. A giant dump of symbols that passes the lean compiler is meaningless besides human beings understanding it.

Qwen 27B is runnable for that price and it can produce patches that work using opencode as a harness. It's obviously not as capable as frontier models but it can do things if you provide the judgement.

How about we give humans access

Have you not seen vend bench?

I think the difference is in math the problem is fully specified and easily verifiable and in programming it's not. I don't agree that we always know we can solve the problem.

But select statements are the most important part, and second to that is the fact that goroutines are low cost user space threads

But it's not exactly a cosmetic change. x++ is semantically different from x; x++; I wonder if clang would make it branchless if you instead write

  if (BLQS_CMP(x, piv)) { *lwr = x; ++lwr; }
    else { *rwr = x; --rwr; }

The difference is post-increment has strange semantics. While the compiler should be able to understand that the value wasn't used and post increment and pre increment are the same I wouldn't be surprised if it tracks that it was post increment and misses some optimizations because it's trying to garuntee post increment semantics.

Although it's true compilers can be very sensitive to exact phrasing triggering specific optimization passes. So it still might not give the branchless version by changing it to pre increment (which is the same as a normal +=1).

The only way to really know is to dig into what optimization passes clang took in both cases and analyze the difference.

You should just have it OCR a screenshot of the PDF that would probably work better

> We don't really know how to program yet, or how to manage our programs. We don't really know what we want to say or how to say it. We don't have good computer languages for expressing what we want to computer to do. We don't know how to think about programming.

I think this is still true today. Software is only just starting and there is a lot of room to find better ways of doing things.

I think the reason writing a compiler is easy today is the theory I learned in compilers class. How to do context free grammars, the concept of abstract syntax trees, the pattern of writing a recursive descent parser and having a lexer that only looks one symbol ahead and has a peek function. On top of that we have experience with lots of languages and type systems to draw from when constructing a new one.

I was just doing some research and apparently all of this stuff was invented around the late 60s and so in the 70s it was still new and by the 90s it was standard practice. The dragon book came out in 1986 and spelled it all out in one place.

Today we have the benefit of knowing the right ideas to use from the start and confidence that if you follow the formula it will all work out.

There's also the major problem of people expecting Google to be right when it tells them something but OpenAI had no starting reputation so it was okay to say "be aware it might be wrong sometimes"

I don't think that's an ongoing debate looks to me that it ended in 2019 https://github.com/golang/go/issues/31440#issuecomment-53724...

Presumably the missile needs GPS to hit the target so if you jam right when the missile is coming in the missile will miss so you can't really jam the warning

Also if you broadcast noise when your missile is about to hit then your own jamming signal acts as an early warning as well, although I guess it wouldn't provide location.

Now the flaps don't melt! The tiles don't fall off!

It's a major overhaul of the design they've been working on for a long time. There was talk of v3 fixing the problems in early v2 test flights. The booster is v3 as well which presumably is why they had some problems. I believe this is also the first time they flew the v3 engines with the plumbing fully integrated in a single piece housing they 3D printed.

I only read the abstract but I got the impression that their solution to this is they have both. They translate all the data as if it was code and if it gets called into they use the translation where if it gets read as memory they use the original.

Edit I found this in the paper

> Elevator sidesteps the code-versus-data determination altogether through an application of superset disassembly [6]: we simultaneously interpret every executable byte offset in the original binary as (i) data and (ii) the start of a potential instruction sequence beginning at that offset, and we build the superset control flow graph from every one of the resulting candidate decodes. Every potential target of indirect jumps, callbacks, or other runtime dispatch mechanisms that cannot be statically analyzed therefore has a corresponding landing point in the rewritten binary. These targets are resolved at runtime through a lookup table from original instruction addresses to translated code addresses that we embed in the final binary.

Not true, they were down because they still use bluesky's relay

Trade secrets once made public don't have any legal protection and I haven't signed any contract with anthropic

Implying that programming is not an actual job that takes years of training and experience

To be clear I don't think the AI can do either job

The champion of compatibility lives on

Yes but the lords are not satisfied with this. They demand the 10x productivity they sold to investors. If you do it this way you will not produce 10x the code.

I'm having trouble understanding to what extent the machine learning used for interfacing with the neurons is doing the learning

In reality it's not that hard for them to work around the constitution e.g. by buying data from private companies

Your cookie banner is very inconvenient and made me leave your website and not read the article

It would be nice to give them some kind of attribution in the readme or something since you know which projects you referenced

A good reason to actually test that you reject man in the middle certs if you rely on TLS in your application

I don't understand, yay updates itself. I've never once had this problem.