• 0 Posts
  • 4 Comments
Joined 1 year ago
cake
Cake day: September 1st, 2023

help-circle
  • The benefits of a free market have been discussed by communists in the past, and newer experiments like the reforms implemented by China make it clear that socialism is compatible with a free market, to very good results.

    Thanks for engaging with OP in a civil fashion, especially when you felt attacked… Anyway, hmu if you want to discuss this in more depth.



  • Yes, that’s true and a better way to look at it, thanks!

    Well, I was amazed by proof systems like Coq or Isabelle, that let one formally verify the correctness of their code. I learnt Coq and coded a few toy projects with it, but doing so felt pretty cumbersome. I looked at other options but none of them had a really good workflow.

    So, I attempted to design one from scratch. I tried to understand Coq’s mathematical foundation and reimplement it into a simpler language with more familiar syntax and a native compiler frontend. But I rushed through it and turns out I had barely scratched the surface of the theory. Not just regarding the proof system, but also with language design in general.

    I did learn a lot though. Since then I’ve been reading more about proof systems and language design in my spare time, and I’ve collected quite the stack of notes and drafts. Recently I’ve begun coding a way more polished version of that project, so on to round two I guess!