[HN Gopher] Verified dynamic programming with S-types in Lean
       ___________________________________________________________________
        
       Verified dynamic programming with S-types in Lean
        
       Author : rck
       Score  : 37 points
       Date   : 2025-06-17 14:28 UTC (3 days ago)
        
 (HTM) web link (tannerduve.github.io)
 (TXT) w3m dump (tannerduve.github.io)
        
       | gugagore wrote:
       | FYI the use of "subtype" here does not, as far as I know, have
       | much connection to the concept in class-based object oriented
       | programming languages.
       | 
       | https://lean-lang.org/doc/reference/latest/Basic-Types/Subty...
       | 
       | A crucial difference between type theory (as its known in Lean)
       | and set theory is that an inhabitant/element is of exactly one
       | type.
        
         | codethief wrote:
         | I'm not quite following. According to the OP and the docs you
         | linked, a subtype is defined by a base type and a predicate. In
         | other words: You can view it as a subset of the set of elements
         | of the base type. That's pretty much the standard definition of
         | a subtype.
         | 
         | Object-oriented programming languages are not _that_ different:
         | The types induced by classes can easily be viewed as sets: A
         | child class is a specialized version of its parent 's class,
         | hence a subtype/subset thereof if you define all the sets by
         | declaring `instanceof` to be their predicate function.
        
           | SkiFire13 wrote:
           | > You can view it as a subset of the set of elements of the
           | base type.
           | 
           | Technically speaking the elements in the supertype are all
           | distinct from the elements in the subtype and viceversa. They
           | are not a subset of the other, hence why it's improper to
           | consider one a subtype of the other.
        
       | jeremyscanvic wrote:
       | Really interesting trick!
        
       | almostgotcaught wrote:
       | This is proof by exhaustion: the "proof" just computes the entire
       | memo table for any n and compares the values in the table with
       | the corresponding return from recursive definition. You could
       | write this same proof in absolutely any language that supports
       | recursion (or not, if you transform to the bottom-up
       | formulation).
        
         | Quekid5 wrote:
         | Not if that language doesn't actually check the totality of
         | your proof and ensures that the base case holds.
        
           | almostgotcaught wrote:
           | 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.
        
       | xnacly wrote:
       | sigma types, hmmm
        
       ___________________________________________________________________
       (page generated 2025-06-20 23:00 UTC)