The way I approach it, it's really more about checking for failures, rather than verifying success. Like a smoke test. I scan over the code and if anything stands out to me as wrong, I point it out. I don't expect to catch everything that's wrong, and indeed I don't (as demonstrated by the fact that other members of the team will review the code and find issues I didn't notice). When the code has failed review, that means there's definitely an issue, but when the code has passed review, my confidence that there are no issues is still basically the same as it was before, only a little bit higher. Maybe I'm doing it wrong, I don't know.

If I had to fully verify that the code was correct when reviewing, applying the same level of scrutiny that I apply to my own code when I'm writing, I feel like I'd spend much longer on it---a similar time to what I'd spend writing on it.

Now with LLM coding, I guess opinions will differ as to how far one needs to fully verify LLM-generated code. If you see LLMs as stochastic parrots without any "real" intelligence, you'll probably have no trust in them and you'll see the code generated by the LLM as being 0% verified, and so as the user of the LLM you then have to do a "review" which is really going from 0% to 100%, not 90% to 100% and so is a much more challenging task. On the other hand, if you see LLMs as genuine intelligences you'd expect that LLMs are verifying the code to some extent as they write it, since after all it's pretty dumb to write a bunch of code for somebody without checking that it works. So in that case, you might see the LLM-generated code as 90% verified already, just as if it was generated by a trusted teammate, and then you can just do your normal review process.

"The exact location of Hyperion is nominally secret but is available via internet search.[12] However, in July 2022, the Redwood Park superintendent closed the entire area around the tree, citing "devastation of the habitat surrounding Hyperion" caused by visitors. Its base was trampled by the overuse and as a result ferns no longer grow around the tree.[13]

Measures to protect the Hyperion tree were officially implemented in 2022 when the National Park Service (NPS) closed public access to its location in Redwood National Park.[14][15] Anyone who gets too close could face up to six months in jail and a $5,000 maximum fine.[13][16][17]"

Allowing uncountably many symbols can be more convenient when you apply logic in other ways, e.g. when doing model theory, but from a foundational perspective when you're doing stuff like that you're not using the "base" logic but rather using the formalized version of logic that you can define within the set theory that you defined using the base logic.

A better way to dispute the unit square diagonal argument for the existence of sqrt(2) would be to argue that squares themselves are unphysical, since all measurements are imprecise and so we can't be sure that any two physical lengths or angles are exactly the same.

But actually, this argument can also be applied to 1 and other discrete quantities. Sure, if I choose the length of some specific ruler as my unit length, then I can be sure that ruler has length 1. But if I look at any other object in the world, I can never say that other object has length exactly 1, due to the imprecision of measurements. Which makes this concept of "length exactly 1" rather limited in usefulness---in that sense, it would be fair to say the exact value of 1 doesn't exist.

Overall I think 1, and the other integers, and even rational numbers via the argument of AIPendant about egg cartons, are straightforwardly physically real as measurements of discrete quantities, but for measurements of continuous quantities I think the argument about the unit square diagonal works to show that rational numbers are no more and no less physically real than sqrt(2).

Obviously, since f(f) = f it should be a -> a as well. But to infer it without actually evaluating it, using the standard Hindley-Milner algorithm, we reason as follows: the two f's can have different specific types, so we introduce a new type variable b. The type of the first f will be a substitution instance of a -> a, the type of the second f will be a substitution instance of b -> b. We introduce a new type variable c for the return type, and solve the equation (a -> a) = ((b -> b) -> c), using unification. This gives us the substitution {a = (b -> b), c = (b -> b)}, and so we see that the return type c is b -> b.

But if we use pattern matching rather than unification, the variables in one of the two sides of the equation (a -> a) = ((b -> b) -> c) are effectively treated as constants referring to atomic types, not variables. Now if we treat the variables on the left side as constants, i.e. we treat a as a constant, we have to match b -> b to the constant a, which is impossible; the type a is atomic, the type b -> b isn't. If we treat the variables on the right side as constants, i.e. we treat b and c as constants, then we have to match a to both b -> b and c, and this means our substitution will have to make b -> b and c equal, which is impossible given that c is an atomic type and b -> b isn't.

I think there is a definite "step up" in complexity between the structures of abstract algebra such as monoids, rings, groups and vector spaces, and monads. All of those algebraic structures are basically just sets equipped with operations satisfying some equations. Monads are endofunctors equipped with natural transformations satisfying some equations. "Endofunctor" and "natural transformation" are considerably more advanced and abstract concepts than "set" and "operation", and they are concepts that belong to category theory (so I don't see how you can read and understand the definition of a monad without that basic level of category theory).

Your time estimates also seem wildly optimistic. A common rule of thumb is that reading a maths textbook at your level takes around an hour per page. I think the definition of a monad can be compared to one page of a textbook. So I'd say it'll take on the order of hours to read and understand the definition of a monad, and that's assuming you're already entirely comfortable with the pre-requisite concepts (natural transformations, etc.)

Think of a computation as a process of changing state. At a given point in time, the computer is in a certain state, the current state. The computation can be described in terms of a function that acts on the current state.

In a deterministic computation, the function takes in the current state, and produces a single state as output which will be the state the computer enters on the next tick.

In a non-deterministic computation, the function takes in the current state and produces a set of states as output. These states are all the possible states the computer might enter on the next tick. We don't know (or just don't care) which one of these states it will enter.

You can model a non-deterministic computation as a deterministic one, by using a list `currentStates` to store the set of all possible current states of the computation. At each "tick", you do `currentStates = flatMap(nextStates, currentStates)` to "progress" the computation. In the end `currentStates` will be the set of all possible end states (and you could do some further processing to choose a specific end state, e.g. at random, if you wish, but you could also just work with the set of end states as a whole).

It's in this sense that "a list is a non-deterministic result", although this is really just one thing a list can represent; a list is a generic data structure which can represent all sorts of things, one of which is a non-deterministic result.

In this respect interviewing is a bit like LeetCode. LeetCode problems and writing code to satisfy business requirements are both "coding" but they're quite different kinds of coding; someone being able to do the former is probably good evidence they can do the latter, but there are also plenty of people who can do the latter without being able to do the former. So it is, in my view, with interviewing vs. interacting with people on the job.

It's not impossible, it just has zero probability of occurring.

(The latter statement holds because for any given n, the set X_n of all strings of length n is finite. So you can count the members of X_0, then count the members of X_1, and so on, and by continuing on in that way you'll eventually count out all members of X. You never run out of numbers to assign to the next set because at each point the set of numbers you've already assigned is finite (it's smaller in size than X_0, ..., X_n combined, for some n).

In fact, even if you allow countably infinitely many phonemes to be used, the X_n sets will still be countable, if not finite, and in that case their union is still countable: to see that, you can take enumerations of each set put them together as columns an a matrix. Even though the matrix is infinite in both dimensions, it has finite diagonals, so you can enumerate its cells by going a diagonal at a time, like this (the numbers reflect the cells' order in the numeration):

    1  3  6  10 15
    2  5  9  14
    4  8  13
    7  12
    11

There's also the fact that `Num` is technically not a type, but a type class, which is like a level above a type: values are organized into types, and types are organized into classes. Though this is more of a limitation of Haskell: conceptually, type classes are just the types of types, but in practice, the way they're implemented means they can't be treated in a uniform way with ordinary types.

So that's why there's a syntactic distinction between `Num a` and `a :: Num`. As for why `Num` comes before `a`, there's certainly a reasonable argument for making it come after, given that we'd read it in English as "a is a Num". I think the reason it comes before is that it's based on the usual function call syntax, which is `f x` in Haskell (similar to `f(x)` in C-style languages, but without requiring the parentheses). `Num` is kind of like a function you call on a type which returns a boolean.