This differs from my own experience with C++. I went from language-lawyer level knowledge (in some parts) while using it heavily (at work, at play and answering Stack Overflow questions on it) to forgetting quite basic stuff after a few years of no use at all. This was all before LLMs were on the scene. With that said, relearning is much faster than learning the first time, as the basic "shape" of things is still there in my mind.
In my defence, even Stroustrup acknowledges the language is too big and complicated, and it's continually getting bigger.
The big initial hump I recall was syntax for writing main and what to #include, then header guards. That, and getting clang up and running in a docker on windows so I could use new C++ features and flags that were blowing up with whatever compiler I got started on. Once I was able to iterate things started coming back quickly.
I always enjoy hearing the thoughts of someone who took a slightly different path (indie game development being a favourite), and isn't committed to advancing some thesis -- pressing me to love this or hate that. It feels like it gives my brain a chance to step back from dopamine- or rage-induced habits and just... connect with other people.
I don't know what will happen either. I hope that you and I and other hardworking, basically good people will continue to have a somewhat meaningful, somewhat pleasant existence in the post-AI world, and I think that might be possible, but I just don't know.
> Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase.
Is it possible that the spec could be factorised into something higher-level and more modular? If not, can you give a flavour of the type of unavoidable esoteric detail? (One area I can see lots of complications is when dealing with versioned data, especially in multiple interacting systems -- naively, correctness needs to be proven for every combination of versions, even if some are never seen.)
> Most of the commercial websites required a Flash blob to deliver full functionality
Being a binary blob is not a strong argument all by itself. chrome.exe, firefox.exe, etc. are also binary blobs. I have no love for Adobe, but that specific criticism is weak.
I think there's a difference between a single-install binary blob to run the entire browser, and a binary blob required to view a single website in the browser. But I don't think it's a huge difference, for sure.
Unless you literally try every possible combination of inputs (which is usually infeasible), property testing can't give you mathematical guarantees about correctness. You can think of it as a halfway house between classic testing and formal verification:
Classic testing: A human comes up with some concrete example inputs for which they know the "right answers" (corresponding outputs). They write code that runs the code under test, gets its actual outputs, and compares them to the desired outputs.
Property testing: A human comes up with a precise way of randomly generating concrete example (input, desired output) pairs. They write some code to describe how to generate the pairs, often using a declarative DSL that describes only constraints on the inputs and outputs, with the understanding that anything not expressly forbidden is permitted, like "The input can be any list of between 0 and 100 integers each between -500 and 500" and "Every integer in the input must appear the same number of times in the output". They then write some more code (often a single line) to ask the computer to use this "spec" to randomly generate, say, 1000 such pairs, or as many pairs as can be checked in 1s. The computer generates the pairs itself, runs the code under test on each input and and checks its output matches the desired output.
Formal verification: A human comes up with a spec that typically describes conditions that must hold for all (input, output) pairs. This may look very similar to, or even exactly like the DSL used for property testing, though in general there are other conditions that can be expressed that cannot be checked with property testing even in principle -- for example, checking that the program always eventually terminates. The main difference is that the code under test is never actually run; instead, the computer analyses the source code itself to attempt mathematically prove that the stated conditions hold. How to actually accomplish this is a field of active research, but one basic approach is called "symbolic execution". To greatly simplify, if we forget about loops and conditionals for a moment, the idea is that we can write down things we know must be true after each statement executes, based on the things we knew must be true before it executed. So for example if x is a variable initially containing any integer (and we ignore overflow) then after the line
x = x * x
runs, we know that x >= 0. To handle conditionals like
if x > 50:
x = 42
something_afterwards(x)
the prover "forks" into two cases: One in which we know for certain that x > 50, one in which we know for certain that x <= 50. At the end of the if statement it then has the task of recombining what is known about the two cases. In this example, the first case lets us conclude that x = 42 by the end, while the second case lets us conclude that x <= 50 by the end, so it could conclude that x <= 50 either way by the time execution reaches something_afterwards(x). Handling loops is trickier but generally involves looking for invariants.
> sometimes they genuinely help OSS, other times they look more like marketing
Whenever companies do things like this, it's both, or at least trying hard to be. To the extent that it's perceived by developers (that is, potential OpenAI customers) as helping OSS, it's effective marketing. This perception may or may not correspond to reality.
I think what's actually happening is that the game only counts your swipe as an input once you lift your finger off the touch screen.
You can kind of get away with that if you're implementing, like, 2048 (although the official version at play2048.co doesn't do this), but it feels way too unresponsive to be usable in an action game.
In my defence, even Stroustrup acknowledges the language is too big and complicated, and it's continually getting bigger.
reply