Nothing in Mathematics is real. It exists only in our heads. By the way, that's a good thing!
You can apply math to many things though, even to programs. You can use it to understand real things. Writing it down doesn’t make it real. Just like unicorns, just because I just wrote it down just now doesn't make it any more real. PKE -----Original Message----- From: bitc-dev [mailto:[email protected]] On Behalf Of Matt Oliveri Sent: Friday, April 03, 2015 11:27 AM To: Discussions about the BitC language Subject: Re: [bitc-dev] Not everything is a type On Fri, Apr 3, 2015 at 2:08 PM, Pal Engstad <[email protected]> wrote: > “A hypothesis is a type, a proof is a program.” > > A program is a set of instructions to be given to a computer. It is a > real thing. Yes. > A proof is a mathematical concept, it has nothing to do with reality, > though it is sometimes useful when it coincides. No, a proof is a way to communicate a mathematical argument. It's written somewhere; it's real. Formal proofs weren't real in practice until they started making proof assistants. The Curry-Howard correspondence points out a syntactic isomorphism between proofs and programs in certain systems. That's what we're talking about. > A type is an abstraction meant to convey meaning to a program for a > certain combinations of bits. Your definition of type is too narrow. Not all type systems are for programming languages. > A hypothesis is a completely random thought that may or may not have > anything to do with reality. True enough, but it behaves syntactically like a variable nonetheless. > PKE > > PS: I’m thinking that someone here has landed far too far into > abstraction Lalaland. After all, this is supposed to be a systems language, > not Haskell. Yeah, we got sidetracked by this ridiculous argument about whether there should be multiple boolean types in a logic. I should probably just let Keean crash and burn. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
