@tmyklebu @pervognsen Another amusing strategy is to deliberately accept incompleteness and restrict the class of proofs you consider to those that basically just correspond to successive unfolding of definitions:
https://madhu.cs.illinois.edu/pldi13.pdf
I'm curious to know the simplest program/property for which this strategy fails.
=> More informations about this toot | View the thread | More toots from zwarich@hachyderm.io
=> View tmyklebu@mastodon.gamedev.place profile | View pervognsen@mastodon.social profile
text/geminiThis content has been proxied by September (ba2dc).