Introduction: Noble Mushtak

Stream: new members

[Noble Mushtak (he/him)]

Hello, I saw this page suggested sending an intro message in this channel, so just wanted to say hi! My name is Noble, and I first learned about proof assistants in college, when I had to formalize a type safety proof when doing research. Yesterday, I just finally finished a type safety proof for an academic language called RichWasm that I've been working on for 3 years, you can see the proofs in this GitHub repo. The experience has gotten me really interested in formalizing proofs, so I am now starting to learn Lean and want to contribute to the mathlib library eventually. Nice to meet everyone here!