@cbaberle @jonmsterling @jcreed @carloangiuli @buchholtz @boarders @danielgratzer @ecavallo @anuytstt @totbwf @amy @ncf @jesper @chrisamaphone @MartinEscardo @jonasfrey @DavidJaz (That's a long list of mentions...)
This looks very nice. It's a topic that I care about, and whenever I contemplated it, I thought I'd end up inventing Isabelle or some such, but with dependently-typed metatheory. These thoughts lead to Andromeda, which was not executed well, unfortunately.
Also, it seems like there is a significant difference in terms of engineering between having a system that can reason about synthetic worlds, and having a system in which users can formulate their own synthetic worlds and use them, If anyone knows how to combine these two, we have a winner.
=> More informations about this toot | View the thread | More toots from andrejbauer@mathstodon.xyz
=> View cbaberle@mathstodon.xyz profile | View jonmsterling@mathstodon.xyz profile | View jcreed@mastodon.social profile | View carloangiuli@mathstodon.xyz profile | View buchholtz@mathstodon.xyz profile | View boarders@mathstodon.xyz profile | View danielgratzer@mathstodon.xyz profile | View ecavallo@mathstodon.xyz profile | View anuytstt@fosstodon.org profile | View totbwf@types.pl profile | View amy@types.pl profile | View ncf@types.pl profile | View jesper@agda.club profile | View chrisamaphone@hci.social profile | View MartinEscardo@mathstodon.xyz profile | View jonasfrey@mathstodon.xyz profile | View DavidJaz@mathstodon.xyz profile
text/geminiThis content has been proxied by September (ba2dc).