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

I've dreamed about making my own language for about 10 years or so. Started out just messing around. My vision for what it would be and its purpose has changed over time. About 2 years ago, I "got serious" about designing and implementing it, though that doesn't mean I've spent a serious amount of time on it yet. But it's happening!

It's a language for the domain of writing and verifying formal proofs. Basically, I didn't enjoy the experience of working with the couple of proof assistants I tried, so I'm doing my own thing. My objective is to create a language where I can document "everything I know" about math, if for no other reason than to prove to myself that I know those things, and to return to that knowledge if it ever slips away.

It's so much fun!



Sounds neat - got any example code you could share?


Not ready to do that yet. But I hope so one day!




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

Search: