banner
satnam6502.bsky.social
Satnam Singh
@satnam6502.bsky.social
2.6K followers 910 following 520 posts
Punjabi-Scottish-American husband and father of two, Haskell hacker at Groq, cook, cyclist, Lost In Music. ∃🇮🇳 ∧ ∀🇬🇧 ∧ ∃🇪🇺 ∧ ∀🇺🇸 #celiac ex-{Microsoft, Google, Facebook, Xilinx, Glasgow} living in Los Altos, California http://raintown.org
raintown.org
Posts Media Videos Starter Packs
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 1d
Oh, I don't know. I am just drawing pretty pictures!
1
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 4d
internal temperature got to 54°C after which I sliced and served.
1
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 4d
skin side of two breasts totaling 600g for 15 minutes, turning the heat down to medium-low as soon as I added the duck breasts to the pan. After 15 minutes of cooking on the skin side (constantly removing the rendered fat) I cooked the flesh side for 6 minutes. After resting for about 7 minutes the
1 1
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 4d
For the hot pan vs. cold pan controversy I am on the side of the hot pan. Seared duck breast with a whisky soy sauce (Oban 14), on a bed of spring onions, asparagus and sugar snap peas (thank you Nick Nairn). I started with a Hestan titanium pan at 200°C and seared the scored salt and pepper
2 8
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 4d
When my daughter was born 22 years ago I never expected to have the following family dinner conversation with her:
Kiran: <a story about getting into trouble with "git add ." at work>
Dad: <Have you considered only using "git add -u ." when using . as an argument?>
4 45
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 8d
No, that’s a variant, a good one.
1
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 9d
Well, my Lava DSL significantly pre-dates Chisel.
1 1
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 9d
The beauty of asking an AI to generate a proof for a lemma (e.g. a formal property about a circuit) is that it can be checked by an external interactive theorem prover (like Lean) to establish whether the AI’s output is actually correct. This is an awesome superpower!
1 8
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 9d
I will work on exploring applications of Aristotle to the formal verification of hardware. This job is a perfect intersection of hardware design and verification, functional programming, formal methods and machine learning, bringing together several threads of my career so far.
1 1 7
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 9d
I have landed my dream job. I’ve just accepted a position at Harmonic, a Palo Alto startup applying AI to formal mathematical reasoning. Harmonic’s Aristotle formal reasoning model achieved Gold Medal level performance at this year’s International Mathematical Olympiad (IMO). harmonic.fun
Harmonic - AI for Formal Mathematical Reasoning
AI for Formal Mathematical Reasoning
harmonic.fun
10 61
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 12d
I am very much looking forward to the Formal Methods (FM) and Artificial Intelligence (AI) workshop next week at SRI in Menlo Park. It's worth going just for the attendance list!
sites.google.com/view/fmxai20...
Atlas Computing presents:
Sep 30 - Oct 2, 2025 SRI International, Menlo Park.
sites.google.com
1 10
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 15d
Produced from a hardware DSL written in Haskell using dependent types and a combinators for computing the layout.
6
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 15d
I did some more hacking to produce a totally floorplanned 64-input sorter circuit on a Xilinx XC7A200T FPGA, on the LHS picture shown as a tight rectangular block, on the RHS a close-up that shows the butterfly wiring pattern.
3 1 8
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 16d
I am a bit more tempted by AI x mathematic x Lean x formal hardware verification.
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 16d
Yet, I still feel the pressure to work, to provide for my family, to have a work identity so my friends will still want to see me. Yes, I know how ridiculous all of this this sound, pathetic even. But I still cant reconcile the disparity between what I think and feel. Forged from a crucible where
8
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 17d
each component that is instantiated. Dependent types in Haskell provide compile time guarantees about the correct size of all the bit-vectors and arrays in the implementation. Many thanks to Lennart Augustsson and @dorchard.bsky.social for help with the dependent types.
5
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 17d
This is what the core of the Haskell Lava DSL implementation looks like. It is a bunch of point-free style recursive combinators that capture the recursive structure and layout of the butterfly network. After evaluation, this produces a SystemVerilog file with layout annotations for
1 6
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 17d
A lovely Xilinx 7-series FPGA chip layout of a sorting network produced from a dependently typed DSL in Haskell. More stuff like this during my keynote talk at ICFP 2025 in October in Singapore. icfp25.sigplan.org/details/icfp...
2 6 60
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 19d
for technical knowledge and skill as I am for my working style and for communication and collaboration. This seems like a much better way of interviewing than the standardized white board coding and system design questions. Fingers crossed for this afternoon!
13
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 19d
it felt like a much better style of interviewing for me, I did not have brain freeze (much) and I did not just speak gibberish in order to have the interview over and done with. The interview this afternoon will involve a two hour problem solving session, and I think I am being interviewed as much
1 4
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 19d
and asked incredibly detailed questions about Verilog semantics (a hardware design language). I was also quizzed in detail about my past projects and I got my laptop out and demonstrated and ran code live. Although I did not necessarily do super well in all of these interviews,
1 2
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 19d
This startup is taking a very different approach to interviewing me. I've gone into their office and basically had "working sessions" with their engineers, discussing various technical topics in depth. One interviewer even brought up a POPL 2025 paper (a top programming languages conference)
1 2
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 19d
One megacorp rejected me after a discussion with a hiring manager (they hired someone else instead). Two megacorps automatically rejected me (I did not even get as far as talking to a recruiter). I've moved onto my second company with a full interview loop this week (last interview this afternoon).
1 2
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 19d
So far I have talked to 25 companies but I've only done a full interview loop with one (8 interviews). Sadly that did not work out (much to my surprise). I also had one "ambush interview" with a company that I thought I was having a more informal chat with.
1 6
satnam6502.bsky.social
Satnam Singh @satnam6502.bsky.social · 28d
actual performance on the job.

I don’t expect companies to change how they interview, and I can’t rewire my brain, so it is what it is. All I can offer is an apology to all the people who have interviewed me over the years and had to endure discomfort due to my brain freeze.
5 4