Lightnews — Scholar-powered news

Satnam Singh

@satnam6502.bsky.social

2.6K followers 920 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

Satnam Singh @satnam6502.bsky.social · 6h

Part of me still expects to spot his ghost wondering around Little India.

Satnam Singh @satnam6502.bsky.social · 6h

This is my first trip to Singapore, but mentions of the place have always loomed large in our family history.

1 6

Satnam Singh @satnam6502.bsky.social · 6h

paving the way for my mother and I to move from India to the UK to join him (he had gone ahead). I was about one and a half at the time my mum and I made the trip. Eventually my mum and I would get British citizenship too, when I was around seven.

1 3

Satnam Singh @satnam6502.bsky.social · 6h

My father lived in Singapore before I was born, and I have been walking the streets wondering if I have retraced any of his steps. As an Indian he was here at the right time to apply for and get a British passport (or some similar document). This was a pivotal moment in our family history,

2 16

Satnam Singh @satnam6502.bsky.social · 6h

The video recording of my ICFP 2025 keynote talk Functional Programming for Hardware Design is up on YouTube. www.youtube.com/watch?v=1oBO...

[ICFP/SPLASH'25] Orchid Plenary Ballroom - ICFP Papers and Events (Oct 13th)

YouTube video by ACM SIGPLAN

www.youtube.com

3 18

Satnam Singh @satnam6502.bsky.social · 7d

Oh, I don't know. I am just drawing pretty pictures!

Satnam Singh @satnam6502.bsky.social · 10d

internal temperature got to 54°C after which I sliced and served.

Satnam Singh @satnam6502.bsky.social · 10d

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

Satnam Singh @satnam6502.bsky.social · 10d

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 9

Satnam Singh @satnam6502.bsky.social · 10d

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 46

Satnam Singh @satnam6502.bsky.social · 14d

No, that’s a variant, a good one.

Satnam Singh @satnam6502.bsky.social · 15d

Well, my Lava DSL significantly pre-dates Chisel.

1 1

Satnam Singh @satnam6502.bsky.social · 15d

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

Satnam Singh @satnam6502.bsky.social · 15d

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

Satnam Singh @satnam6502.bsky.social · 15d

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

Satnam Singh @satnam6502.bsky.social · 18d

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

Satnam Singh @satnam6502.bsky.social · 21d

Produced from a hardware DSL written in Haskell using dependent types and a combinators for computing the layout.

Satnam Singh @satnam6502.bsky.social · 21d

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

Satnam Singh @satnam6502.bsky.social · 22d

I am a bit more tempted by AI x mathematic x Lean x formal hardware verification.

Satnam Singh @satnam6502.bsky.social · 22d

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

Satnam Singh @satnam6502.bsky.social · 23d

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.

Satnam Singh @satnam6502.bsky.social · 23d

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

Satnam Singh @satnam6502.bsky.social · 23d

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

Satnam Singh @satnam6502.bsky.social · 25d

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!

Satnam Singh @satnam6502.bsky.social · 25d

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