texoport.in
typescript person
he/him
2,666 posts
510 followers
306 following
Getting Started
Active Commenter
comment in response to
post
also, how on earth is Lean's in-editor experience so much nicer than most mainstream languages with faaar bigger ecosystems?
comment in response to
post
incredible!
comment in response to
post
check out her LeanTeX repo
github.com/kiranandcode...
comment in response to
post
fuck, that's glorious 🥹
comment in response to
post
i'm still pretty new to Lean's metaprogramming, do you have any examples that are public? I think this aspect of Lean almost excites me more than the theorem proving side of things
comment in response to
post
i wish they hadn't ended firefox os (or microsoft, the windows phone)
comment in response to
post
this hasn't been updated yet, sigh killedbymozilla.com
comment in response to
post
oh no that's not dumb enough
expect to feel the urge to want to send me a virtual punch when i'm done with it in ~1 business week
comment in response to
post
ya, i wish we had a nicer syntax for it but it was surprisingly easy to get it working! github.com/saiashirwad/...
comment in response to
post
lean4 will solve all my problems (really)
comment in response to
post
i'm also looking forward to getting better at lean4's metaprogramming so i could do wonderful things like this:
grammar MyLang where
expr := num | var | binop expr op expr
op := "+" | "*" | "-"
comment in response to
post
ive never used happy, do you like one of those more than the other?
comment in response to
post
i should write a blog on piss driven development
comment in response to
post
far too many things to do and faaar too little time
comment in response to
post
not to be confused with my *other* side quest to piss off *all* programmers (except maybe folks that wrangle binaries for a living)
comment in response to
post
lenses are awesome! i don't get to use them much as they're the wrong abstraction to use in TS (though you can _totally_ make them work), but i've been sneaking them into all of my new haskell code
comment in response to
post
100%
it's also far more expressive as a melodic instrument than the piano will ever be
comment in response to
post
the applicative notation in haskell used with parser combinators really fucks with my head though i've recently reluctantly started using them more
comment in response to
post
you could totally make them work without undecipherable nomenclature!
comment in response to
post
i wish you had equal parts aussie, british, and german in your accent, would've been a thing of beauty
comment in response to
post
I wondered if the German part ever crept into your English accent
comment in response to
post
i always imagined you with a British accent though
comment in response to
post
comment in response to
post
i was a casualty of the Kraut-Badempanada wars
comment in response to
post
lmao ya
comment in response to
post
✅
comment in response to
post
that's the only result that showed up when i googled it but i thought it maybe had something to do with the Russian Z, though I couldn't imagine why I'd be on such a list lol
comment in response to
post
Someone needs to be the David Sancho of the Lean4 world
comment in response to
post
bsky.app/profile/texo...
comment in response to
post
i'm thinking it's because i follow badempanada, or liked a couple of his posts
comment in response to
post
... what's DayZ?
comment in response to
post
i don't understand this particular one
comment in response to
post
*holds up cup that says "liberal tears"*
comment in response to
post
i'm on a list called Tankies and their Supporters!
comment in response to
post
all 5 of them
comment in response to
post
i'm forbidden by my religion from prodding deeper. if the elders knew about the times i read the v8 blog they would excommunicate me for being a heretic
comment in response to
post
as a sun baked south indian, i would freeze in that temperature
comment in response to
post
turning your beautiful mathematician language into my Lean Mean Web Dev Machine
comment in response to
post
side side quest: effects library like zio/effect-ts in lean4. i don't really understand lean4's concurrency primitives yet and don't know if it has continuations etc, but .... 🤞
comment in response to
post
now that i've been fucking around with Lean4 again I think it could honestly do most of what I wanted out of ur/web. I've been learning metaprogramming in Lean so I can have JSX in it
comment in response to
post
one more functional webdev language that compiles to javascript*
javascript is my assembly, oliver
comment in response to
post
speaking of which, the only reason i got into compilers/type theory, albeit passively, was because i wanted to make something very similar to ur/web without some of the annoying bits ... so i'll blame him for distracting me from my happy webdev world
comment in response to
post
when i email him to enquire about the current state of ur/web, and ask if he's comfortable talking about future plans, etc, i'll add that to the P.S
comment in response to
post
ugh it's chlipala, not chipala. i've been spelling his name wrong all this time
🥲