[HN Gopher] The Deep Link Equating Math Proofs and Computer Prog...
       ___________________________________________________________________
        
       The Deep Link Equating Math Proofs and Computer Programs
        
       Author : digital55
       Score  : 47 points
       Date   : 2023-10-11 14:52 UTC (1 hours ago)
        
 (HTM) web link (www.quantamagazine.org)
 (TXT) w3m dump (www.quantamagazine.org)
        
       | caycep wrote:
       | was this something to do with Djykstra's work?
        
       | boxfire wrote:
       | Programming in dependent types with univalence (Homotopy Type
       | Theory) is an awesome way to see this realized.
       | 
       | The typing statement has to be proven by realizing the
       | isomorphism demanded by substitution. You are more than anything
       | directly proving what you claim in the type. Since proof is
       | isomorphism here, the computation in terms of lowering the body
       | of the definition to a concrete set of instructions is execution
       | of your proof! (possibly machine code or just abstract in a
       | virtual machine like STG). The constructive world is really nice.
       | I hope the future builds here and dependent types with univalence
       | is made easier and more efficient.
        
       | qsort wrote:
       | If you want to see how the Curry-Howard isomorphism works in
       | practice, this is a very accessible introduction:
       | https://groups.seas.harvard.edu/courses/cs152/2021sp/lecture...
        
       ___________________________________________________________________
       (page generated 2023-10-11 16:00 UTC)