OSDev.org

I suspect that the Jetsons film predicts the future of programming (in attachment):
What programming languages ​​and operating systems will be used in the future of programming to according Jetsons film?

Ah, The Future! There are some nice flying cars in the works, some in the past, and one in recent production which looks like an Austin Metro (why???), but I don't know about programming... and I haven't seen the film. (I ought to.) To me, it looks like the trouble is every language which gets popular (and some which don't) ends up weighed down with a morass of complexity. Python's a good language in many ways, but it's got 6 billion functions for network operations, WHY??? The few basic functions which can do 90% of what you'd want to do with a network are lost in the mess.

I didn't want to understand the soup lines line when I was a kid. These days, I'm okay with satirizing The Future. I don't think we saw The Jetsons in 80s Britain, or maybe they stopped repeating it when I was still very young, but we did have a lot of books pretending to be factual and portraying the future with the same shiny aesthetic but with styles updated to some degree. I loved books of all kinds and I loved anything futuristic, so I really fell for this.

I once saw art of a woman's hand working what looked like a big old desk calculator with a caption something like, "The proof-based programming language makes it easy for her to program." I think it was from the 60s, all things considered. (And I now realised it used sexism to increase its impact.) I do remember reading such hopes for proof-based programming languages in various places in the 80s and 90s, but the practical works never mentioned it. As an adult, I looked into proof rather hopefully, but soon sided with Knuth who said, "What if there are bugs in the proof?" It's such an obvious objection, but devotees of the sect of proof aren't listening. They are doing some interesting (or at least complicated) things with Agda, but it seems it'll be a long time before they even make Agda into a stable language. It's more a thing to be experimented on than experimented with. A friend of mine recently got into it. I think he's now trying to produce a whole stable language and library starting with Peano arithmetic - an immense undertaking. I still think bugs can be introduced in the proofs at higher level, but he's having fun.

Now I'm imagining a Future world where all programming languages are provable and all programs provably correct. The hype got it adopted, just like general computer hype in the 60s. Also like 60s computers,* provability isn't half as good as it's made out to be. So in this Future, all the boss guys believe in provability but all the code monkies still have to deal with bugs. After a while the truth emerges​. (You've seen this, it happens every 5-10 years, just before computing finds a new stupid to fall for.) So now research is undertaken to find a way to prove proofs. Eventually, they're successful and the cycle repeats. Proofception! (Because one visual entertainment reference isn't enough.)

*: "Paperless office" indeed! I know a guy who worked for a company who fell for that in the 60s. I can reasonably do paperless today, but it was rough in the 00s thanks to low resolution screens and ps/pdf everywhere; a terrible combination! It started to get usable at 1600x1200, then I got a 1680x1050 screen which was half-way back to being too small. I should have kept the 1600x1200 screen but a 21" CRT is a massive thing, it had a warped mask, I wanted my just-renovated flat to be all nice, and most of all I wanted the trappings of progress. Stupid reasons! I didn't find another monitor so comfortable to look at until my 4k I bought this year. That's 14 years in which I could have had a better monitor, but I gave it up for "progress". Okay the mask was warped, which means the colours went wrong in some parts of the screen, but a large chunk was correct and it was comfortable to read and work with. It would even go up to 2048x1536 if I wanted it to, but unlike any LCD screen, I didn't have to have insane resolution to read comfortably. And the height is very valuable; widescreens less than about 28-30" are disgusting little letterboxes. When I had two widescreens I tried having one vertical, but then it was too narrow! Besides, the one which went vertically easily was also the one with better colour and viewing angle so I wanted it for games. That Benq was a *huge* mistake. Between that and Linux, I have a much dimmer view of "progress" these days... but I still get excited by the aesthetic. I like my iBook Key Lime SE despte everything. I should put a high-res screen in it; really should have done that in the 00s when I found a tutorial for it.