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
