https://drcicero.github.io/topics/ Recent content in Topics on My New Hugo Site Hugo -- gohugo.io en-us https://drcicero.github.io/topics/choreographic/ Mon, 01 Jan 0001 00:00:00 +0000 https://drcicero.github.io/topics/choreographic/ ← Back to Home Write a whole distributed system as one script, and let the compiler split it up. A distributed system is normally written as many separate programs, one per participant, which have to agree on a protocol that exists nowhere in the code. Choreographic programming inverts this: you write the interaction once, as a single program that names every participant, and a compiler projects it onto the individual endpoints. https://drcicero.github.io/topics/incremental/ Mon, 01 Jan 0001 00:00:00 +0000 https://drcicero.github.io/topics/incremental/ ← Back to Home Compilers that turn plain functional code into computations that redo only what changed. Most programs throw away their own work. Change one cell of a matrix, one row of a table, one node of a tree, and the whole computation runs again from scratch. Incremental programming asks the compiler to do better: from an ordinary functional program, derive a second program that consumes a change to the input and produces the corresponding change to the output, reusing everything that was already computed. https://drcicero.github.io/topics/types-and-proofs/ Mon, 01 Jan 0001 00:00:00 +0000 https://drcicero.github.io/topics/types-and-proofs/ ← Back to Home Types catch bugs before a program runs, and stop humans and bots alike from doing nonsense. A type system is a negotiation. The programmer wants to write what they mean; the compiler wants a guarantee it can actually check. Push too hard on the guarantee and the notation turns rigid (effects marshalled one per line, motives spelled out by hand). Push too hard on convenience and the guarantee evaporates. https://drcicero.github.io/topics/machine-learning/ Mon, 01 Jan 0001 00:00:00 +0000 https://drcicero.github.io/topics/machine-learning/ ← Back to Home Derive and prove what ML frameworks hard-code, and search for the equations that generated the data. Machine learning runs on a small set of operations (differentiate this, invert that, multiply these arrays) that a compiler ought to be able to derive rather than have a human write out by hand. That is one half of the work here: taking the transformations deep learning frameworks hard-code and giving them a proper functional foundation, so they can be optimized aggressively and proved correct rather than trusted.