macleginn

Yes, this makes sense. Although you will probably have to implement at least some of the middle layer's functionality, which means (at least for me) roughly the same level of debugging complexity when coming back to your own code later.

"A modern web application typically puts a web server like nginx in front and reverse-proxies to an application server written in another language like Ruby, Python, Go, or Rust. That always felt a bit strange to me: you essentially have two web servers, and one of them is also responsible for your business logic." -- Is the fundamental difference here that the business-logic binary is not always running but gets spun out with each request? This looks like a relatively minor thing, to be honest.

You made the right choice, but importantly, this is a single generation of uni graduates. Each subsequent generation finds it harder to leave, and even if all who would could, there will still be enough human capital for the war effort and then some. For comparison, brain drain is even stronger in Israel, proportionally.

By "it" people in such cases are usually referring to the NL proof. It seems nobody has any hope of undersanding AI-generated Lean code any more, if only due to volume.

The thing is, you often see people saying, ‘They have a Lean cert, so it has to be correct, even if I don't understand it.’

This is not even an option in the UK. Communication felonies (dangerous speech, threatening behaviour) only demand potential audience.

"And second, before we create systems significantly more capable than the ones we have today, we need new science to ensure that more capable models (and their successors) will make safe choices when we aren’t looking." – Which science will never materialise because with blackbox models reaching an opaque optimisation peak one needs to first build the model and track its behaviour before being able to properly understand it and mitigate the risks.

I am glad that this topic gets more attention, but the article itself doesn't provide any real analysis and could use some proof-reading. In its current shape, it's borderline engagement farming.

I am an emigrant now. When I was still living in my East European country of origin, my wife and I would regularly hold parties. We liked going to other peoples’ places more than hosting but most of our friends would not throw parties themselves, so we had to fill the gap.