Curator of Mastodon.art fediblock :newt: (npub1wc2…4sk7) Scathach (npub1lc8…92pf) I wouldn't call it proof-assistant though — it has no tactics or any interactive features (relying on emacs for proof search can't be taken seriously)
if it's not to write actual programs then I don't really know what it's for, other than 80-20 reimplementation of something that existed before with reduced functionality
Andrew /
npub1l4…4cyh6
2024-02-03 14:09:47
in reply to nevent1q…ngjt
Author Public Key
npub1l4zwh56tscqnqc3y8k48a7s7jsqzy3kap30tj4uah63v3n5jprysp4cyh6Published at
2024-02-03 14:09:47Event JSON
{
"id": "b532de4013cc2cc81729d6dddcabe674be19259a1e0013ce6ba9d32d5de47db8",
"pubkey": "fd44ebd34b86013062243daa7efa1e94002246dd0c5eb9579dbea2c8ce9208c9",
"created_at": 1706965787,
"kind": 1,
"tags": [
[
"p",
"7615614e4ed5bed70847ce5a32852a79ddde9dce8a650059f31546d61c1ad441",
"wss://relay.mostr.pub"
],
[
"p",
"fe0e47aae1904586530e886b769fecc0a12fc476c4d30d22dc2be04c8d494693",
"wss://relay.mostr.pub"
],
[
"e",
"11aa5a035a1cbdf095cbb2089ff09c45e05e31f884289088bc165345997fe8e7",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://stereophonic.space/objects/17d5dbef-acc3-4bb7-a395-511f54d2dba9",
"activitypub"
]
],
"content": "nostr:npub1wc2kznjw6kldwzz8eedr9pf208waa8ww3fjsqk0nz4rdv8q663qswt4sk7 nostr:npub1lc8y02hpjpzcv5cw3p4hd8lvczsjl3rkcnfs6gku90syer2fg6fslg92pf I wouldn't call it proof-assistant though — it has no tactics or any interactive features (relying on emacs for proof search can't be taken seriously)\nif it's not to write actual programs then I don't really know what it's for, other than 80-20 reimplementation of something that existed before with reduced functionality",
"sig": "a4fdeabbd6f294c0f2f28a672b0995cd4c61fda445f292616e0b42b6dc1d81fb856fb61267f4d4311ab56a4a2105a8a5dcc2539f9e0edba60ce6d260d84a6138"
}