[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)