Check out SeL4 (a proven correct micro kernel used by billions of devices worldwide) and CompCert (a proven correct C compiler used by Airbus).

One of the best reads on AI I have read so far. Bravo!

I am using AI at work. And it definitely makes me (say) 10% more effective.

However my #1 productivity tool is still a custom code generator I have been using for years. It routinely generates 90+% of the code needed to write a typical biz web application, leaving just the business logic.

No AI. Just straightforward high-level-spec-to-server-client-DB code that is 100% trusted and proven in battle.

A great overview of the problems we all know we have. And zero new ideas on how to fix it.

Developing a "new kind of programming system" has been done many times before. Think case tools, functional programming, object oriented programming, CORBA, DDD, etc. etc. etc.

So best of luck but I highly recommend not investing your time unless you have at least one truly new idea that will change the outcome for the better.

Take away automation from our factories and farmers and see how quickly civilisation will fall apart.

Learning how to program from tutorials is like learning how to ride a bike from watching YouTube videos.

You kinda feel that you are learning something but you only truly learn when you have to do it from scratch.

The vast majority of people using UI's want predictability. Not "guess how this UI works!" games where you have to click on things at random to figure out how the UI works.

If you are an UI designer and want to create art then fine do that in your spare time. But at work be a professional and make the UI predictable and functional above all else.

Whatever you do don't waste your time on the "Dragon" book.

Google "recursive descent parsing" and it will tell you everything you need to know about the front-end of a compiler.

Google "My First Language Frontend with LLVM" and it will teach you the other half.

"The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct (and now has a PR addressing)."

In other words, the code was proven correct according to spec by LEAN. Which is exactly what LEAN claims to do.

Recognise that waiting for motivation to strike is a bad idea.

Instead just get started with the smallest possible step you can just about manage to do. And then do another smallest step. A lot of times you almost automatically keep going and the motivation then arrives.

Maybe the first step is to create a basic "Hello World" application. And then a few empty functions/methods that flesh out what the app needs to do. Then maybe a few of those methods/functions are really easy to do (or AI can write them for you) so you quickly do those. Etc.