boolean and infinates, HOL Lite, types and random musings

by josephzizys

another very breif post noting the interesting article here talking about formal proofs and computers, the type structure reminded me of the seemingly irreducible dualism in this world between the boolean and the infinate, between the analogue and the digital, its a tantilising shape in the field of ‘vibes’, one that I am not usually attracted to, being more generally a person that is pluralistic or monistic in my thinking about ‘underlying metephors’, but every now ant then something sparks the ‘dualist’ circuit in my brain, and this article did.