Working Notes: a commonplace notebook for recording & exploring ideas.
Home. Site Map. Subscribe. More at expLog.
type:: #StrangeLoop2023
Proofs and programs
Topos Institute
Revolution in the sky
in math
in computation
1600s galileo, copernicus figure out about the position of the earth and sun / published
died in house arrest
1835 were removed from inquisition index
~300 year revolution
Revolution in Mathematics
19th-20th century beginning
algebra/etc. changes happened this century
curry-howard correspondence
proofs as types, 1908 --
PWL 2015 curry howard correspondence youtube
lambda calculus <-> cartesian closed categories <-> intuitionistic propositional logic <->
proofs as propositions wadler
hilbert: consistent, complete, conservative, decidable
godel: incompleteness theorem
liberalized version of hilbert's program: make notions as intuitively clear
lenses...
can help with automatic differetiation
— Kunal