Comment on Verified dynamic programming with Σ-types in LeanparentComments−Quekid51yNot if that language doesn't actually check the totality of your proof and ensures that the base case holds.−almostgotcaught1yi don't know what you're saying - here is the proof that is described in the article:1. build a table tab[n]2. check that for every i, tab[i] == maxDollars_spec[i]if you take the latter approach i proposed (bottom up) there is nothing to check the totality of.
Comments
Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.
i don't know what you're saying - here is the proof that is described in the article:
1. build a table tab[n]
2. check that for every i, tab[i] == maxDollars_spec[i]
if you take the latter approach i proposed (bottom up) there is nothing to check the totality of.