five favorite things about computers
avril 14, as played by a human (lil data) expressed with a programming language (tidalcycles, derivative of haskell). there is real emotion here, and it isn’t programmed so much as generated, a harmonization between man and machine.
the lambda calculus.
imagine that your only model of the world is a box. you put things into the box, one at a time, then take one thing out. everything you put in is also a box, into which you can place more things.
if something is true, you place two items in the box then remove the first. (λa. λb. a.) a and b enter and a leaves. false is represented when b leaves: (λa. λb. b.).
to count, again place two items in the box. the second item you placed in the large box is placed in and removed from a smaller box a number of times equal to your count. (λs. λx. s (s (s (s … x)))). to put the name of a box around another is to put the inner box through the outer.
to determine if many items are true you can compose them.
(λa. λb. (a b (λx. λy. y.))). if a is true then b is tested and false (as above) otherwise. this system, though one can painstaking construct, model and express everything - it just has to be coaxed out of the machinery.fructure. this is a vision of a new way of programming, one that is composable, beginner friendly and actively engaging. it’s one of the most promising steps towards interacting with our computers using tools more powerful than plain text.
generative art. another harmonization between man, math, and machine - the user expresses a compact algorithm, often simple and elegant in nature, that generates a series of semirandom, user-guided points, either static or presented as an animation. when graphed over time, this produces work that can touch the natural world.
theorem proving. formal verification technology allows us to guarantee program correctness - so long as the properties proved are adequate - and therefore can be used to both justify prior mathematical results and ensure the safety of our most critical systems. on a large scale, it’s incredibly powerful - and when used simply, it’s as elegant as the math it represents.