this one was too easy 😆
| foundations | constructive, univalent |
| gh | https://github.com/jcreedcmu |
@jcreed
- 563 Followers
- 229 Following
- 4.5K Posts
theorems, types, tunes, typefaces, terms-of-art, tropes, technicalities. [en/eo, +ε es/zh/fr/pl/jp]
ok, I managed to make a minimal native android app with 'capacitor', which is apparently the spiritual descendant of 'cordova'. Reminds me how much pain java development always seems to entail. Nonetheless it works and I can get vibration on notifications, even.
whoops, this was meant to be a link to https://hci.social/@chrisamaphone/116307319860900149
fun little trivia game, I got
catfishing.net
#643 - 7/10
🐈🐈🐟🐟🐟
🐈🐈🐈🐈🐈
Ugh, I got lovely light-weight notifications working via either mobile firefox or chrome with https://github.com/jcreedcmu/notifier/ but then it seems like both firefox and chrome have made it impossible to have these notifications cause vibration. Which was exactly what I wanted to make it possible for things happening on the desktop to actually let me know asynchronously when I step away from the computer...
@edwinb Somewhere buried in here was the idea that traversal of a term while it is being initially typechecked would match very closely the traversal of the same term "executing" as the typechecker for its own arguments
@edwinb nor is this something that is *directly* yet implementable in 6502... but I was trying to get some sort of system together with various stacks such that you could imagine each token as it is parsed doing a limited amount of work at a time, very forthily.
RE: https://mastodon.social/@jcreed/116303446377766919
Ok, due to @edwinb mentioning the idea of "dependently typed language on 8-bit computer" I have at least *visually* cleaned up my old experiment from a couple of years ago, here: https://jcreedcmu.github.io/twelf-nes/
But to be completely honest I don't really remember how the thing worked that well. I am pretty sure it could manage to type-check first-order terms, but the invariants even then were kind of subtle and frequently changing during development...
broccoli soup (https://www.webtoons.com/en/canvas/broccoli-soup/list?title_no=625936) is a webcomic that has some cosy mid-2000s weird webcomic vibes. which is just what I needed today
