Introduction: Hesper (WebGPU) & Sparkle (Hardware)

Stream: new members

[junji hashimoto]

Hi everyone, I'm Junji Hashimoto. I previously contributed to Hasktorch(Haskell bindings for PyTorch), and now I'm diving into Lean 4.

I'm currently developing two projects:

1. Hesper: A DNN framework using WebGPU with verification. https://github.com/Verilean/hesper
2. Sparkle: An RTL generator with verification. https://github.com/Verilean/sparkle

My goal is to connect CPU, GPU, and hardware through formal verification. Both projects are still in the alpha stage, so if you have any advice or feedback, I would really appreciate it.

Lean 4 is great! Thanks.

[Artur Lojewski]

Hello Junji!

I really like your projects and the connection to Lean. Are you aware that Harmonic has a sponsorship program:

https://harmonic.fun/news#blog-post-mathematician-sponsorships

Maybe you want to talk to Mr. @Satnam Singh at Harmonic because he invented Lava (https://github.com/satnam6502/xilinx-lava).

[junji hashimoto]

@Artur Lojewski

Thank you so much for the information, Artur!

To be honest, I wasn't aware of Harmonic's sponsorship program until you mentioned it. It sounds like a fantastic initiative.

I have great respect for Mr. Satnam Singh and his pioneering work on Lava. His research has been a huge inspiration for my Sparkle project, so I would be honored to speak with him.

I will apply for the sponsorship program right away. Could you please let me know the best way to get in touch with Satnam?

Best regards, Junji

[Satnam Singh]

Happy to talk! satnam6502@gmail.com

Cheers,

Satnam

[junji hashimoto]

@Satnam Singh
Thank you, Satnam!
I am honored to have the opportunity to talk with you. I will send an email to satnam6502@gmail.com shortly.