logoalt Hacker News

seanhunteryesterday at 5:36 PM2 repliesview on HN

Fair to say that perhaps isn't selling it as much as you may think. It looks like perl that has been written by someone who is in the process of having a stroke.


Replies

7373737373yesterday at 6:01 PM

How would you improve it? (Also note that this is not the language mathematicians actually work with - that's more like https://www.youtube.com/watch?v=b-RfoUuQpAQ)

Similarly, for Metamath Zero, MM1 compiles down to the MM0 base language: https://www.youtube.com/watch?v=A7WfrW7-ifw

I think it's just a neat example that helps one understand how the verifier itself works at the most fundamental level.

jjgreenyesterday at 7:46 PM

Or Raku.