#41 The Value of PL (and) Education - Satnam Singh
Type Theory Forall
Deep Dive
What are the key milestones in Satnam Singh's career in both academia and industry?
Satnam Singh has a diverse career spanning academia and industry. He worked at Google, Facebook, Microsoft, Microsoft Research, and Xilinx. He has been a lecturer at the University of Glasgow, Birmingham, and the University of California. His work includes functional programming in hardware design, formal verification, and contributions to Kubernetes. Currently, he works at Groq, applying functional programming to design silicon for machine learning.
How did Satnam Singh's upbringing influence his career in technology?
Satnam Singh grew up in a poor farming family in Punjab, India, and later moved to the UK. His parents were illiterate, and he initially spoke only Punjabi. He developed an early interest in technology through a book on mathematics and later through a BBC microcomputer. His passion for understanding how computers work led him to pursue a career in computing, eventually earning a PhD and transitioning into academia and industry.
Why did Satnam Singh transition from academia to industry?
Satnam Singh transitioned from academia to industry due to the high stress, low pay, and long hours associated with being a junior academic in the UK. He found the work exhausting and financially unsustainable. An opportunity at Xilinx, where he worked on practical applications of functional programming in hardware design, led him to leave academia and join the industry, where he felt freer to innovate without the constraints of academic publishing.
What is the significance of functional programming in hardware design according to Satnam Singh?
Functional programming in hardware design allows for greater agility in exploring design spaces and composing complex systems. It enables the creation of parameterized descriptions of hardware, which can be evaluated quickly to find the best design. Functional programming also provides better support for formal verification, ensuring that composed components work as expected. This approach was successfully used in projects like the BlueSpec-designed machine learning chip at Google, which worked flawlessly on the first attempt.
What are the challenges Satnam Singh faced with bullying in the workplace?
Satnam Singh faced bullying from a senior manager at a company, which led to a difficult experience with HR. He learned that HR's primary role is to protect the company, not the employee. This experience taught him to recognize early warning signs of bullying and to seek help or move away from toxic situations. He has since written about his experiences to raise awareness and support others facing similar issues.
How does Satnam Singh view the future of hardware verification?
Satnam Singh believes that hardware verification is currently in a good state, with the hardware industry leading the software industry in the use of LTL-inspired property checking. However, he envisions a future where total verification is possible, with complete specifications and proofs that entire systems conform to those specifications. He highlights the ACL2 system as a promising tool for practical formal verification in hardware.
What advice does Satnam Singh have for those interested in programming languages and formal methods?
Satnam Singh emphasizes the value of studying programming languages and formal methods, as it provides a mental toolbox for problem-solving that is applicable across various fields. He encourages people to engage with the PL community, attend conferences, and build professional and personal relationships. He also highlights the importance of mentorship and inclusivity in fostering a supportive and innovative community.
- Satnam Singh's background and upbringing in a poor farming family in India.
- Immigration to the UK at a young age and the challenges faced.
- The pivotal role of education and government support in his success.
- His transition from academia to industry and back again.
- The importance of education in bridging social gaps.
Shownotes Transcript