A different paradigm of programming, which lies as a bridge between pragmatic programming and theoretical mathematics. A few notes on this particular subject:
- It all starts from lambda-calculus, which defines the least amount of definations needed to create a turing-complete programming language. Quite interesting to view it’s connections to every other programming concepts. Equally interesting is an alternative way of viewing computation.
- Going further, there’s the Curry-Howard correspondance, another interesting result of mathematically defining computation through lambda-calculus, which provides us a way to define mathematical structures and proofs in a programming language (absolute/formal terms). This is a good reference to understand in detail, while this is a course for the same.
Applications
Some rather cool applications that I’ve come across, which lead me into the rabbit hole that this concept is:
- Bend, is an application of the above-mentioned alternative view of computation, made to use GPUs efficiently, automatically.
- Electric is a clojure DSL which tries to solves the problem of communication between front and back end in web applications, by automating the seperation of concerns programmatically.
- Eiger, an attempt at formalizing law in haskell.
- This paper/blog generalizes the transformer architecture, in a way that it could work on arbitrary input shapes, not just vectors.