IRC channel logs

<matrix_bridge><Christoph> oriansj: Defining types bit by bit touches on a question I have long time now: What exactly is a type? How is 'type' defined? Bartosz Milewski models types with sets, but types cannot be sets because so many proof assistents make a point of working with types instead of sets. I've never seen axioms for types like Zermelo Fraenkel for sets. But I once saw a PhD thesis where a type by definition had an...

<matrix_bridge>... encoding of its values specified (and I curse myself for having lost the reference). And now you wish for a programming language that allows defining types down to their bit representation, that's why I ask you.

<oriansj>Christoph: the simplest way I know how to express the concepts of types in programming languages is as a bounded set of states with positional information which delivers some meaning to hardware.

<oriansj>For example the following hardware: 1bit <=> 1 pixel graphics display; if you rearrange the bits inside of a byte (say from big to little endian) the image no longer appears correctly. If the property of an operation produces (say add) results in some effect; if its behavior changes the output we don't get the picture we expect but changes in its behavior that don't change the output (such as shuffling around internal operations to

<oriansj>speed things up) we are fine with (assuming such shuffling doesn't result in side channels that leak private keys)

<oriansj>they either must map to physical hardware requirements (like an ALU's big bit endian and little byte endian immediate format) or to human abstractions which are simple to reason about (Like Lisp's *WONDERFUL* rational number types)

<oriansj>but those abstractions must ultimately have transformations and mappings that reduce down to the primitive types supported directly in hardware.

<oriansj>and one could include primitive types that hardware doesn't directly support and thus incur a penalty for the multiple operations required to simulate them.

<oriansj>I also believe there is a book called: Types and Programming Languages by Benjamin C. Pierce on the topic

<webczat>question, someone here definitely knows: how to compile relocatable gcc? which is not dependent on the directory it's put in?

<oriansj>which depends upon external libraries or no?

<webczat>it's static linked. it's more about the search paths

<webczat>the --with-sysroot makes it depend on paths.

<oriansj>(also you need to include binutils and a glibc binary) well there is rpath

<webczat>oriansj: this is a statically linked musl based gcc.

<webczat>actually the problem is mostly header search

<oriansj>you can just pass where you want it to look for headers/libraries

<matrix_bridge><Andrius Štikonas> It's probably just easier to fake path for GCC using namespaces

<oriansj>-I /$PATH/

<webczat>oriansj: i was just wondering how does it normally look like when you make a portable native toolchain like available on http://musl.cc ... used it once but don't remember if it was path dependent or required passing flags to find stdlib includes

<webczat>namespace tricks are really nice tricks. i love namespaces.

<oriansj>plan 9 has a good few more than Linux but then again it isn't the most loved Unix

<webczat>oriansj: for example?

<oriansj>Well right now by a large margin the most loved Unix is Linux

IRC channel logs

2024-03-03.log