Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Your project is cool too! I haven't tried Lean yet but have done some similar formalization in Agda.

I went with Haskell as my meta-language because I'm specifically trying to focus on language implementation rather then formal analysis and proofs.

I have everything from the README other then linear types, row polymorphism, and case-trees implemented outside the repo (and some in the main/old folder). I haven't gotten them into the repo yet because I want to make sure the implementations are succinct and decently documented.

I want to move onto a 1lab style presentation with substantially more documentation at a later date.



Consider applying for YC's Fall 2025 batch! Applications are open till Aug 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: