Formally Verifying PBS Kids with Lean4

Tech can be as much fun as ever in the right hands and it can be the base for a kids show I'd have loved to see as a child. All it takes is for the right people to make and publish it. It'd be based around what you - yes, you - can do to build, repair and design machines to do the sort of things children may want to do from the silly to the potentially useful. It would mention the 'AI' thing as one of the ways computers can help but it would not concentrate on it since the point would be to give children self-confidence in what they can do with limited means.

Tech is as fun, and even more fun than it used to be, in my opinion.

The software and hardware limitations are a fun challenge (albeit becoming ever so more hard to break) and you can have kids enter at any stage of technology: from a simple terminal only system, to a rpi, or modern computers. You have games, robotics, embedded systems, etc. that are order of magnitude easier to pick up and with far more tutorials (back in my days, I only could find 1 complete tutorial to make games, in C++ + OpenGL and only in English).

I personally wouldn't start anyone off straight with LLMs as I believe it takes away a bit of the self exploration and taking it as slow as needed.

Call me an optimist but I believe being a parent and getting a kid interested in tech hasn't been easier, especially since the social stigma has long since diminished.

> I don't mean we need one, just that tech is no longer fun

Or maybe the whole thing goes in cycles. For example: the 1980's were a fairly significant time for computer themed books for kids (teaching us how to program from a variety of angles). I don't remember that much kid oriented stuff in the 1990's, but then there was the panic of kids not knowing how to program in the early 2000's, which may have been where those shows came from.

Another factor is that a lot of kid's programming is recycled from generation to generation (either outright rebroadcast or developing new programming under the same franchise). That's really hard to do with tech oriented stuff. Even futuristic gadgets would appear to be dated.

> we don't have any kids shows with an AI theme today

There plenty where the toys are alive, or one of the characters is a robot or a computer.