julesh on Nostr: The crazy thing about Lean is that from a technically slightly inferior foundation ...
The crazy thing about Lean is that from a technically slightly inferior foundation they're successfully hacking stuff that's obviously decades away from being feasible to engineer properly. Like, literally nobody knows how to make a typechecker that doesn't totally shit itself as soon as you put a function call in an index, but they apparently just ignore the problem and charge forwards. It's genuinely impressive, it reminds me of Youtube videos like "Can you beat Dark Souls using only a wet pool noodle?"
Published at
2025-02-05 12:34:12Event JSON
{
"id": "8605f0d585733004570d82d87766cc27c490b73470cac5f4722049f2a64289c5",
"pubkey": "75c7d1f69389e4c76276bb851aea7f54265d145c7a39678589cfd62ce26ae9b3",
"created_at": 1738758852,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/@julesh/113951300187154713",
"web"
],
[
"proxy",
"https://mathstodon.xyz/users/julesh/statuses/113951300187154713",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/julesh/statuses/113951300187154713",
"pink.momostr"
],
[
"-"
]
],
"content": "The crazy thing about Lean is that from a technically slightly inferior foundation they're successfully hacking stuff that's obviously decades away from being feasible to engineer properly. Like, literally nobody knows how to make a typechecker that doesn't totally shit itself as soon as you put a function call in an index, but they apparently just ignore the problem and charge forwards. It's genuinely impressive, it reminds me of Youtube videos like \"Can you beat Dark Souls using only a wet pool noodle?\"",
"sig": "ad63845e4432f86aa67760be609cf3624c8aa2052498d91a1802586d334e18282dabfbf6d6f0b55542fb562e241190c59e318b025e73c57bca5b57140cf17a42"
}
