Replying to
@secretasianman@types.pl
@secretasianman@types.pl from PL Twitter a long time ago
Remote
joomy
@joomy@functional.cafe
researcher at Bloomberg 🅱️. somehow a computer doctor. 🐅 posts about functional programming, metaprogramming, proof assistants, and sometimes about linguistics, or Turkey.
0
Followers
0
Following
18
Posts
Joined August 07, 2023
location:
New York City
website:
twitter:
github:
Posts
Replying to
@joomy@functional.cafe
@mudri@mathstodon.xyz wait, actually, I have been informed that the few hours might be because the game is extremely slow, and it gets progressively slower as you play... in that case, no credit to my game :) I'll try to fix it.
Replying to
@mudri@mathstodon.xyz
@mudri@mathstodon.xyz if a single game took a few hours, that’s pretty good!
Replying to
@joomy@functional.cafe
btw these are all available in your browser now, thanks to Emscripten and WebAssembly:
http://joomy.korkutblech.com/rocqman
http://joomy.korkutblech.com/rocqsweeper
http://joomy.korkutblech.com/reversirocq
web developers, please stop putting popups on text selection. I will never use a feature like this to share an excerpt from a text on social media. let me select text in peace, that's just how I read things.
stress eating? yes, I also emphasize the importance of eating.
Replying to
@mudri@mathstodon.xyz
Replying to
@joomy@functional.cafe
I discovered that my wife was a big fan of minesweeper so I'm continuing with my wife's favorites: Reversi / Othello this time. (I'm terrible at playing it but she's very good, she beats me every time.) https://github.com/joom/reversirocq
for the game AI, I used the coinductive game tree unfolding described in my CPP '26 paper (though an alpha-beta pruned version): https://dl.acm.org/doi/10.1145/3779031.3779091
Replying to
@joomy@functional.cafe
and this time I got nerdsniped into making a minesweeper game in Rocq (with proofs about the game logic and interactions!): https://github.com/joom/rocqsweeper
Replying to
@joomy@functional.cafe
dammit i should have released this on april fools day
Replying to
@chrisamaphone@hci.social
@chrisamaphone@hci.social @markusde@mathstodon.xyz @tom7@mastodon.social I did not know! this makes the LFMan video funnier for sure.
(having not grown up here, I have zero knowledge of any children's entertainment from American culture anyway, regardless of age)
Replying to
@markusde@mathstodon.xyz
@markusde@mathstodon.xyz thanks to @tom7@mastodon.social for the inspiration: https://www.youtube.com/watch?v=6pKjOudDDEc
Rocq is Pacman complete!
see Rocqman, a Pacman implementation (with some proofs!) in Rocq, extracted to C++ via Crane: https://github.com/joom/rocqman
just submitted a paper to OOPSLA about Kip (my programming language in Turkish where grammatical case and mood are part of the type system)! 🎉 given how niche the topic is, I don't have super high hopes but you never know! also, I personally think the work is really cool so I care a bit less. I'll keep trying until I find the right reviewers / venue for this paper.
the draft is available here: https://joomy.korkutblech.com/papers/kip.pdf
Replying to
@dancer_storm@mathstodon.xyz
@dancer_storm@mathstodon.xyz it's from an interview in Turkish with Ali Akurgal, though I cannot find exactly when and where it was published. I am attaching the newspaper clipping to this toot. I translated it to English (with the help of ChatGPT) so that I could post here.
the story was also featured quite often in Turkish media and social media. here are some links with the same story:
https://web.archive.org/web/20120317215245/www.kaldiracetkisi.com/?p=443
https://eksisozluk.com/metreyle-yazilim-satmak--3297121
https://www.haberturk.com/yazarlar/fatih-altayli-1001/2701300-2-bin-metre-yazilim
someone else at the same company telling the same story for a documentary: https://www.youtube.com/watch?v=UPrOCb0rmvY
the UNIX v4 tape reminded me of this story by Ali Akurgal about Turkish bureaucracy:
Do you know what the unit of software is? A meter! Do you know why? In 1992, we did our first software export at Netaş. We wrote the software, pressed a button, and via the satellite dish on the roof, at the incredible speed of 128 kb/s, we sent it to England. We sent the invoice by postal mail. $2M arrived at the bank. 3-4 months passed, and tax inspectors came. They said, “You sent an invoice for $2M?” “Yes,” we said. “This money has been paid?” they asked. “Yes,” we said. “But there is no goods export; this is fictitious export,” they said! So we took the tax inspectors to R&D and sat them in front of a computer. “Would you press this ‘Enter’ key?” we asked. One of them pressed it, then asked, “What happened?” “You just made a $300k export, and we’ll send its invoice too, and that will be paid as well,” we said. The man felt terrible because he had become an accomplice! Then we explained how software is written, what a satellite connection is, and how much this is worth. They said, “We understand, but there has to be a physical goods export; that’s what the regulations require.” So we said: “Let’s record this software onto tape (there were no CDs back then—nor cassettes; we used ½-inch tapes) and send that.” Happy to have found a solution, they said, “Okay, record it and send it.” The software filled two reels, which were handed to a customs broker, who took them to customs and started the export procedure. The customs officer processed things and at one point asked, “Where are the trucks?” The broker said, “There are no trucks—this is all there is,” and pointed to the tape reels on the desk. The customs officer said, “These two envelopes can’t be worth $2M; I can’t process this.” We went to court, an expert committee examined whether the two reels were worth $2M. Fortunately, they ruled that they were, and we were saved from the charge of fictitious export. The same broker took the same two reels to the same customs officer, with the court ruling, and restarted the procedure. However, during the process, the unit price, quantity, and total price of the exported goods had to be entered—as per the regulations. To avoid dragging things out further, they looked at the envelope, saw that it contained tape, estimated how many meters of tape there are on one reel, and concluded that we had exported 1k to 2k meters of software. So the unit of software became the meter.
Replying to
@mspstrath@mastodon.acm.org
@mspstrath@mastodon.acm.org @jfdm@discuss.systems Hi @jfdm@discuss.systems, I'm working on a paper about unfolding rose trees (though nothing generic, and nothing about ASTs). Is this going to be a paper eventually? Is there a draft I can take a look at? Or maybe even slides would be nice. Then I could know how to compare and cite your work.