nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqa97ytde5dtp079mk499scnxwc3jyrvkvu89gm60cgxc9gfdugk2sapetws (nprofile…etws) tbh Lean 4 achieves a very good score on this topic with a lot of efforts into optimization going there (caching parts of the proofs, etc.) but I can understand the other side of the argument
it's particularly complicated when working on very large scale projects, e.g., https://github.com/AeneasVerif/aeneas
Raito Bezarius
npub1t2…w5ty4
2025-05-14 21:00:47 UTC
in reply to nevent1q…vm0x
Author Public Key
npub1t2c07cksmsemlfwr8qxej8n9pexz3w2f7m2jfch0wurgar4lxl2shw5ty4Seen on
wss://relay.ditto.pubPublished at
2025-05-14 21:00:47 UTCEvent JSON
{
"id": "d83c63cd01d9a4184c4de81019502f81c43c4e03ccce7938c506473776bbf4e1",
"pubkey": "5ab0ff62d0dc33bfa5c3380d991e650e4c28b949f6d524e2ef77068e8ebf37d5",
"created_at": 1747256447,
"kind": 1,
"tags": [
[
"p",
"e97c45b7346ac2ff1776a94b0c4ccec46441b2cce1ca8de9f841b05425bc4595",
"wss://relay.mostr.pub"
],
[
"p",
"b5b38e998fabb0a93c88bce6ac3fb70cf8f9b5a55e87e8bef3d2bc6156d48a37",
"wss://relay.mostr.pub"
],
[
"e",
"4144cfa75188e5960d0be8c267e808cc58553eaf3af8222b0b6709f32e9c46e8",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://nixos.paris/users/raito/statuses/114508198536762248",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqa97ytde5dtp079mk499scnxwc3jyrvkvu89gm60cgxc9gfdugk2sapetws tbh Lean 4 achieves a very good score on this topic with a lot of efforts into optimization going there (caching parts of the proofs, etc.) but I can understand the other side of the argument\n\nit's particularly complicated when working on very large scale projects, e.g., https://github.com/AeneasVerif/aeneas",
"sig": "025ad57064cd4541473572128e80f79cfa3e2508153dfd18628a4abca666aecf3e7fd29f32efaa729c9c6a02ab9c7cbf6b492671c2bb27d3923a3654fac809f1"
}