joomy @joomy@types.pl
- homepage
- http://joomy.korkutblech.com
- http://twitter.com/vowelharmony
- GitHub
- http://github.com/joom
PhD student in programming languages at Princeton. 🐅
I post about functional programming, metaprogramming, proof assistants / IDEs, and sometimes about linguistics, or Turkish politics and Turkey.
Joined Nov 2022
anyone have any cool computer science themed ex libris examples / ideas?
(in case you don't know what that is: https://en.wikipedia.org/wiki/Ex_Libris_(bookplate) )
wait I just realized pton actually makes teaching evaluations public for students who want to take the course in the future, which means there's no reason I can't post them here for bragging rights
joomy
boosted
@arclight
Excel is not a spreadsheet. Excel is a full-featured virtual machine running a smalltalk-inspired REPL whose display layer happens to resemble a spreadsheet.
Something like a third of the world’s money goes through Excel every single day, and the reason you don’t think Excel is a Real Programming Language is because if we admitted that, we’d have to admit that most of the most important software in the world was written by underpaid women in pink collar jobs, and we can’t have that.
joomy
boosted
It’s very funny to me that the dominant Twentieth Century conception of AI was a slightly awkward nerd with an inhuman mastery of facts and logic, when what we actually got is smooth-talking bullshit artists who can’t do eighth-grade math.
today in things I'd never learn if it weren't for my native English speaker wife: the origin of the name "tater tots".
how was I supposed to connect "tater" to potato and "tot" to toddler?
aaaaa my advisor just told me I should put together a thesis committee this week, that I'm ready to do my thesis proposal presentation in a month or so and defend in september 
trying to make speech bubbles in LaTeX to show vernacular commands sent to Coq and the response that comes from Coq like a conversation. this is a TikZ nightmare.
I got my teaching evaluations for the fall semester in the morning.
they're all so wonderful that I've been thinking about them throughout the day. I've never gotten a teaching award they give to TAs but this is enough to make me happy.
the feeling when the compiler goes "it's an undeclared universe but maybe it's a a bugged tactic, idk dawg ¯\_(ツ)_/¯"
I never thought I'd have to solve hard metaprogramming problems when I decided to write a thesis on ... metaprogramming techniques for FFI verification.
question: in a review of the paper I wrote about the Proof Tree Builder ( https://proof-tree-builder.github.io/ ), I am told that calling it a proof assistant is "somewhat misleading with respect to the proof assistants Lean, Coq or Isabelle" and "a bit of an overstatement". (these are from two different reviewers)
Is this true? A toy programming language or an educational, limited programming language still gets to call itself a programming language, why isn't the same true for proof assistants? Or should I ignore that comment? 🤨
joomy
boosted
let’s all take a moment to appreciate the semiotic beauty of the 🫶 emoji, a digital representation of a human body part creating a gesture to represent another human body part representing love
trying to learn how to write Visual Studio Code plugins, but the simplest example of TreeView (a building block for foldable trees in the sidebar) is a plugin that shows the current cr*ptoc*rr*ncy prices, so I don't want to star the repo and have it appear in my followers' feeds. 
the fountain on campus is frozen. it looks so tempting, I just want to slide on it ⛸🛷
joomy
boosted
How did I never realize that running a DFA on a string is described by a fold:
In functional programming terms a DFA consists of
1. A finite state type State
2. An initial state s : State
3. A transition function step : State -> Token -> State
4. A predicate accepts? : State -> bool
Then running the DFA on a string (toks : List Token) is precisely
accepts? (foldl toks s step)
got too excited and applied for a job at a certain code search company that also has a lot of editor plugins for integration etc.
it took them only 2 days to reject me 
proposal to switch from egg store proximity to eggnog store proximity for the holiday season 🥚
joomy
boosted
When your spouse asks you to pick up a white ceramic whale menorah at Target and you have to actually ask whether it’s for Hanukkah or Twitter social commentary.
But why not both?
“There were only enough microservices to last for one night, but they lasted for eight nights.”
seriously though, I'm hoping to finish grad school around September 2023 (or at least by the end of 2023) so I do need an industry job. I'm interviewing with a bunch of places already but given the job market right now, I probably should have alternative plans.
- homepage
- http://joomy.korkutblech.com
- http://twitter.com/vowelharmony
- GitHub
- http://github.com/joom
PhD student in programming languages at Princeton. 🐅
I post about functional programming, metaprogramming, proof assistants / IDEs, and sometimes about linguistics, or Turkish politics and Turkey.
Joined Nov 2022
