←back to thread

Systems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods

(queue.acm.org)
167 points yarapavan | 3 comments | 01 Apr 25 14:59 UTC | HN request time: 0.635s | source
Show context
OhMeadhbh ◴[01 Apr 25 16:06 UTC] No.43548441[source]▶
I find this highly unlikely. My first day at Amazon I encountered an engineer puzzling over a perfect sine wave in a graph. After looking at the scale I made the comment "oh. you're using 5 minute metrics." Their response was "how could you figure that out just by looking at the graph?" When I replied "Queuing theory and control theory," their response was "what's that?"

Since then, Amazon's hiring practices have only gotten worse. Can you invert a tree? Can you respond "tree" or "hash map" when you're asked what is the best data structure for a specific situation? Can you solve a riddle or code an ill-explained l33tcode problem? Are you sure you can parse HTML with regexes? You're Amazon material.

Did you pay attention to the lecture about formal proofs. TLA+ or Coq/Kami? That's great, but it won't help you get a job at Amazon.

The idea that formal proofs are used anywhere but the most obscure corners of AWS is laughable.

Although... it is a nice paper. Props to Amazon for supporting Ph.D.'s doing pure research that will never impact AWS' systems or processes.

replies(7): >>43549053 #>>43549089 #>>43549401 #>>43549462 #>>43549563 #>>43550279 #>>43552944 #
1. scubbo ◴[01 Apr 25 17:32 UTC] No.43549462[source]▶
They specifically mention "the P team at AWS". The two following things are perfectly able to be simultaneously true:

* The average Amazon engineer is not expected to have awareness of CS fundamentals that go beyond LeetCode-y challenges

* The average Amazon engineer builds using tools which are each developed by a small core team who _are_ expected to know those fundamentals, and who package up those concepts to be usefully usable without full understanding

(I did 10 years on CDO, and my experience matches yours when interacting with my peers, but every time I interacted with the actual Builder Tools teams I was very aware that lived in different worlds)

replies(1): >>43549689 #
2. nextos ◴[01 Apr 25 17:56 UTC] No.43549689[source]▶
> The average Amazon engineer is not expected to have awareness of CS fundamentals that go beyond LeetCode-y challenges

I find this a bit unsettling. There are dozens of great CS schools in the US. Even non-elite BSc programs in EU sometimes teach formal methods.

There are also some good introductory books now, e.g. [1]. Perhaps its time to interview more on concepts and less on algorithmic tricks favored by LeetCode?

I doubt current undergrads can't go beyond LeetCode-like challenges.

[1] Formal Methods, An Appetizer. https://link.springer.com/book/10.1007/978-3-030-05156-3

replies(1): >>43550333 #
3. retrocryptid ◴[01 Apr 25 19:09 UTC] No.43550333[source]▶
Modern CS programs teach to what they perceive to be the interview their students will encounter after graduation: what is a tree data structure, how to craft a SQL query and how to calculate a CRC with a python library. More advanced CS/CE departments still teach discrete math and compilers/parsing for students intending to go to grad schools.

My experience with recent CS grads is it's easier to hire Art and Political Science grads and take the time to teach them programming and all it's fundamentals. At least they won't argue with you when you tell them not to use regexes to parse HTML.