yuppiemephisto
Joined 7 years ago
Karma
425
Submissions
80
Member since
May 30
Recent submissions
Comment · 5 months ago
Different Aaronson
Comment · 5 months ago
Where did you have 10k omakase?
Comment · 5 months ago
I love the creator Evan. Enthusiasm, intelligence, focus.
Comment · 6 months ago
some combo of implicit pride and laziness. sorry, i'll fix it up
Comment · 6 months ago
i agree about this point, i think this is one of the ways extensible syntax can save (or damn, like in this case) you
Comment · 6 months ago
i was just messing with you guys, but now i'm feeling a bit more motivated
Comment · 6 months ago
actually i think syntax is incredibly important, but i think i'm approaching it from a viewpoint that's even more syntactic than lisp macros, which in practice tend to center around parens syntactically still. racket a notable exception (and good, but not perfectable lang, one of the inspirations for my remark). typed racket is good but is not culturally central enough. but yeah, i do believe types are [inevitable](https://www.youtube.com/watch?v=0AQdSZqGXz4)
https://reservoir.lean-lang.org/@strata-org/Strata isn't done, but its goal is to let one build whole languages that can look like whatever you like. ones for little kids maybe
syntax matters for normal ppl even more than semantics in some ways since semantics can be optimized and refined on the backend, but everyone is (de)limited by their vocabulary
Comment · 6 months ago
lean IS that language https://github.com/alok/LeanPlot
Comment · 6 months ago
https://alok.github.io/assets/lean-position-paper.pdf
i talked about the lisp curse in this old paper. it's rough but explicitly mentions it
Comment · 8 months ago
I do a form of literate programming for code review to help read AI code. I use [Lean 4](lean-lang.org) and its doc tool [Verso](https://github.com/leanprover/verso/) and have it explain the code through a literate essay. It is integrated with Lean and gets proper typechecking etc which I find helpful.
Comment · 8 months ago
lean 4
Comment · 9 months ago
Unrelated, but I am literally listening to Rolandskvadet right now and reading your username was a trip