413 karma · joined February 4, 2014
There are a couple of quality of life features missing (most notably is record update syntax), but I really enjoy that the core language has not changed in 25 years.
Mechanized proof checkers leverage this idea to enable users to specify formal proofs as programs.
[1]: https://en.wikipedia.org/wiki/Nyquist_(programming_language)
So the first priority is getting the change to a readable state. I'm not talking about nits, I'm talking about minimizing the cognitive overhead to truly understand what the code is doing.
That being said, it is also easy to identify nits during this phase. In codebases that have collections of best practices, this often helps to ensure that the change is expressed in terms of a common vocabulary. Once this pass is done, the reviewer can usually better understand the intent of the changes.
I can recommend some resources in that vein (maybe they'll be useful if you/the reader have a software background):
The most frequently recommended book from a software perspective is "Computer Systems: A Programmer's Perspective" (http://csapp.cs.cmu.edu/3e/home.html).
For a nice gentle intro, you can also read "The Elements of Computing Systems" (https://mitpress.mit.edu/books/elements-computing-systems) that accompanies a course called "Nand2Tetris".
George Hotz also compiled a list of topics to cover to learn the computing stack from bottom-to-top (https://github.com/geohot/fromthetransistor).
These resources are mostly software-oriented, so they wouldn't give you much insight into modern chip fabrication, but if you're coming from a software background, may prove to be useful for building on what you already know.
I'm really curious what could have happened to cause it to collapse so catastrophically when it withstood far more traffic just ~12 hours earlier.
The whole of aip.dev is a collection of API design principles published by Google that are externally relevant. Many of the proposals pertain specifically to gRPC-style APIs.
I've personally found gRPC APIs to be pleasant relative to many HTTP APIs since the use of an IDL can be helpful when interacting with such APIs. I don't have enough GraphQL experience to make any conclusions on that comparison. But the sense that I get is that GraphQL may be more appropriate once you reach a certain scale but is probably overused when a simpler technology would suffice.
Disclaimer: I work for Google but the views I express are my own and not necessarily those of my employer.
I am also partial to explicit error handling over exceptions, and there is a lot to like about absl::Status (and absl::StatusOr).
Disclaimer: I work for Google but the views expressed are my own and don't necessarily reflect those of my employer.
I hadn't seen a great type-safe way to support ad hoc polymorphism until I read about [modular implicits][1] in OCaml. In situations where there is a reasonable module that satisfies a specified signature for the type of an argument, the module can be inferred.
When you have immutability guarantees (like in many functional programming languages like ML or Haskell) you can avoid making copies by sharing the parts of the data structure that don't change.
If this kind of thing interests you, you should check out Chris Okasaki's book "Purely Functional Data Structures".
One of the most important aspects of code review culture isn't really mentioned in the post: requiring at least one additional approval on a PR ensures that at least 2 people are familiar with a piece of code. This helps increase the bus factor on the project and ensures that knowledge transfer and developer velocity can be maintained.
Additionally, the dialogue that occurs during code review can serve as additional documentation into why certain choices were made. I use the blame layer all of the time to try to better understand the context of a particular piece of code. Being able to read through the review for the PR that contained a line of code is often incredibly useful for being able to gain context.
Most of my day job is spent reading C++ (I write some, too) and it is more terrifying than boring. Understanding when certain errors can (and do) occur and when to optimize for performance over readability is really, really hard.
I believe that Rust, Go and TypeScript have gained a lot of popularity because they are boring to read. Even OCaml has gained a ton of popularity because it is boring to read.
C, C++, python and JavaScript: not boring to read, you constantly need to be on your toes.
This also makes collaboration really hard. Types are a form of documentation. But unlike comments, types are enforced by the compiler. Invariably, lots of comments in a codebase are wrong. Many of those probably started out correct but the code changed and the comment didn't.
Relying on this type of behavior when it isn't required is somewhat of an anti-pattern. And can often lead to mindlessly copying the results of an implementation in tests.
A quick aside: any sort of generic ordered container that supports O(n) iteration must necessarily require O(n log n) work to construct in the average case. So the asymptotic complexity is necessarily the same as sorting the keys of a hash map with undefined iteration order to artificially create a defined order.
It isn't too hard to simulate the behavior of insertion order iteration by maintaining an array alongside the hash map. And surprisingly enough, space and runtime complexity is practically identical to containers that implement insertion order iteration ;-)
https://ai.googleblog.com/2006/06/extra-extra-read-all-about...
Others posted similar things, but imagine that you're a female PhD candidate and your male advisor asks you: "How familiar are you with Coq?" or "Are you good with Coq?"
Sure, the advisor could have asked "How familiar are you with the theorem prover Coq?" but it shouldn't be necessary to do so.
It seems petty and childish to be considering a name change over this, but it is far from unprecedented (e.g. "Beaver College" changed their name to "Arcadia University" in 2001). Having a more utterable name can lead to more widespread use and discussion of the tool with laypeople.
On the other hand, if the vaccine reduces the transmissibility of the virus, then everybody collectively benefits from each additional vaccination.
If you are familiar with "Classical" logic, constructive math omits the law of excluded middle (e.g. "A or not A" must be true). In ZFC, the axiom of choice is omitted.
This leads to proofs that are not only a verification of some idea but also gives you the mechanism to compute the evidence. This is often described as "the computational content of proofs" and is especially valuable in the context of the Curry-Howard isomorphism: for every proof, there is a corresponding program (and vice-versa). This is the basis for formal verification of constructive proofs. When creating a proof in Coq, you are actually writing the corresponding program. And you can even extract the program in another general purpose programming language (usually OCaml in the context of Coq, but Haskell is also supported).
Exactly. When you bungle the early response it increases the urgency for vaccine administration.
A lot of these rules exist for the purpose of having a consistent rule. With modern tooling, there is virtually no difference between tabs and spaces. What is important is to have some rule to avoid the constant bikeshedding that would occur if there wasn't one.