+++
title = 'Stuff I Learnt This Year: 2018'
date = 2018-11-09T12:08:42+05:30
draft = false
tags = [""]
description = ""
# For twitter cards, see https://github.com/mtn/cocoa-eh-hugo-theme/wiki/Twitter-cards
meta_img = "/images/image.jpg"
# For hacker news and lobsters builtin links, see github.com/mtn/cocoa-eh-hugo-theme/wiki/Social-Links
hacker_news_id = ""
lobsters_id = ""
+++
# Introduction
I chronicle the broad strokes of new things I've picked up this
year. Some musing, some book reviews, and some ramblings contained within.
I hope you enjoy the ride.
# Coq
Coq is a language that can be used for proving theorems, both mathematical, and
proofs of programs.
A concrete example of doing something like this is implementing quicksort --- why
would you trust your implementation? Maybe there's a weird corner case you missed. In `Coq`,
one can actually implement not just quicksort, but also a **proof** of quicksort, which
is then checked by the Coq compiler. So, we can write _programs we trust_.
Some of the triumphs of Coq include:
- [A mechanized proof of the four color theorem](https://www.ams.org/notices/200811/tx081101382p.pdf),
which was a hard graph theory proof that proceeded by tedious case analysis. We
now trust the proof much more, since the Coq compiler has accepted that we have
covered all cases exhaustively
- [CompCert, a verified C compiler](http://compcert.inria.fr/), which is a C compiler written in Coq,
which also comes with a proof of correctness --- that is, the semantics of the high
level program written in C is the same as the semantics of the low level assembly
that is generated by `CompCert`.
I've wanted to learn Coq for a while now, since I think this is where math
will eventually head -- we will have all our proofs formally verified,
so that we can actually trust what we're doing in really complex math
proofs (the [abc conjecture](https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/) comes to mind, where the debate has been raging
for the last couple of years about the supposed correctness of a complicated proof)
My aim is to implement a formally verified __optimising compiler__ --
that is, a compiler that performs non-trivial transformations (such as
those on loops), which are not performed by `CompCert` so far.
These are difficult to prove, since a proof of correctness of a
program transformation must be proven to be correct for _all_ input
programs.
I've been writing a _lot_ of Coq this year. I essentially started
the year knowing no Coq, and am now ending the year being comfortable with it,
and having a couple minor bugfixes into coq, which feels great!
## [Book: Software foundations](https://softwarefoundations.cis.upenn.edu/)
**link to my solutions: [software foundations solution](https://github.com/bollu/software-foundations-solutions)**
Software foundations is a 3 volume collection which shows how to use `Coq`
to prove properties about programs. This is definitely **the** book to learn `Coq` from -
it's well structured, and has lots of great exercises. Doing the exercises was what
basically taught me the language, which is a style of learning I really enjoy.
## [Book: Certified programming with dependent types](http://adam.chlipala.net/cpdt/)
This is a kind of a "next steps" from software foundations,
which focuses on Adam Chlipala's style of proofs, which
relies heavily on "proof automation" --- that is, the ability to
write small programs (called tactics) that automate the proof for you!
An extreme example is called `omega`/`lia`, that uses some math to automatically
solve linear equations for you. That is, given some equations such as:
```
forall (x: natural), x + 1 > x
```
one simply needs to type `lia.`, which then proceeds to perform the
correct proof for you.
I found the book well written, but still rough to read, since
it does do some things that are actually complicated :)
However, it's a great reference for the more advanced parts of Coq,
and I think it's required reading to be able to use Coq effectively.
## [Project: Dependence analysis for a toy language](https://github.com/bollu/dependence-analysis-coq/)
This was my first `Coq` projet, and it really shows. I've used Coq in
the most naive way possible, but it was fun to get something out the
door, and actually prove things with it!
## [Long term project: PolyIR](https://github.com/bollu/polyir)
The `README` for the project explains it well in my opinion, but the
TL;DR is that to perform loop optimisations, modern compilers are
experimenting with a class of techniques called as polyhedral
optimisation, where one represents loops using integer polyhedra.
Some success stories are the [Polly project for LLVM](), and
Facebook's [Tensor comprehension library]()
`PolyIR` is a Coq project that talks about the meaning of programs
using polyhedra, and also hopes to prove theorems that are requireed
for the machinery of polyhedral compilation to work.
## [Library: SCEV](https://github.com/bollu/scev-coq)
**[Paper link: Expediting chains of recurrences](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.43.8188&rep=rep1&type=pdf)**
`SCEV` is an implementation in `gcc` and `llvm`, about a theory that
allows one to reason about recurrences. This Coq library is an
implementation of the original paper, with most of the lemmas proven.
Once I've proven all of them, I want to upload the package on
coq-extras, so there's a SCEV formalization in Coq. I think it's a
good milestone to have in a new environment to publish a package,
so you know the full toolchain.
## [Pull requests / issues into Coq](https://github.com/coq/coq/issues?utf8=%E2%9C%93&q=author%3Abollu+)
I began by submitting documentation style PRs. I've gradually begun to
read the source code in bits and pieces. I don't really understand the
codebase, but it's been fun to spelunk.
I really enjoyed helping around in the Coq community, the people are
super friendly, and I learnt a *lot* by hanging around the gitter
channel.
## VE-LLVM
**[Project page](https://github.com/vellvm/vellvm)**
**[My PRs/issues](https://github.com/vellvm/vellvm/issues?utf8=%E2%9C%93&q=author%3Abollu)**
`VE-LLVM` (verified LLVM, also a pun on "vellum") is a project that aims
to provide a reference semantics of LLVM on Coq, to allow people to implement
optimisation passes over LLVM, as well as verify these passes.
Due to my interest in formalizing polyhedral compilation, I wound up reading
the `vellvm` source code, since I wanted to see how they verify LLVM syntax.
After all, my grand plan is to have a fully verified `LLVM -> polyhedra -> LLVM` toolchain
at hand.
# The Barvinok algorithm:
**[Book: integer points in polyhedra](https://bookstore.ams.org/emszlec-9)**
**[My presentation slides](https://github.com/bollu/barvinok/blob/master/slides.pdf)**
The barvinok algorithm is an extremely interesting algorithm, which can be
used to "count integer points in polyhedra". That's a mouthful, so let's unpack
that. The basic idea is this:
Let's say I hand you the description of a rectangle as follows:
```
0 <= x
x <= 10
0 <= y
y <= 10
```
I then ask you "how many `(x, y)` points exists in the given polyhedra, where
`x, y ∈ Z`? The answer in this case is `10 * 10 = 100`. However, this easily
gets way more complicated in higher dimensions, with the general intuitition
that "integer stuff === lattice stuff === hard".
The barvinok algorithm was a breakthrough algorithm that showed how to perform
such a point counting in a method that's polynomial in the number of
constraints for a fixed dimension.
I spent the first half of the year chugging through the book, and finally
ended up in me giving a presentation on the material. It was really fun,
and I got to learn a _lot_ of cool theorems about the structure of polyhedra,
and convex geometry.
I'd love to get the chance to explore this stuff in more detail at some point
in time.
# Physics: Gauge theory
Gauge theory is a language of physics, where one analyzes systems
based on the symmetries these systems posess. As a birds eye view, one
can write the physics of a system in terms of a particular function
called as the _Lagrangian_. Next, physicists study symmetries of this
Lagrangian, from which they derive _conservation laws_. If you've
done any physics, you'll know that conservation laws are the bread and
butter of many deep ideas.
There's a deep theorem in physics called [Noether's theorem](https://en.wikipedia.org/wiki/Noether%27s_theorem),
which precisely describes this correspondence between symmetry and
conservation.
I took a course on gauge theory. While the course was too handwavy for
my taste, I did get to appreciate a lot of the ideas, and I at least
now know the vocabulary behind this stuff. I was reeling at how
difficult the course was initially, and still am to be honest.
Going from not knowing Maxwell's equations to knowing the version
of Maxwell's equations written in tensorial form was quite an adventure
to say the least, but the course paid off. I know believe I know what
symmetry breaking means (handwavily), and that makes me happy.
- [Link to my incomplete, poorly written lecture notes](https://github.com/bollu/subject-notes/blob/master/physics/main.pdf)
# Complexity theory / Algorithms / Crypto
I learnt a good bit of theoretical computer science over the last two
semesters, mostly thanks to good courses. I took courses on complexity theory,
algorithms, and information security.
The information security course was great, not only because I learnt a bunch
of awesome things, but also becase it forced me to learn `LaTeX` properly!
I now have a reasonable view of the basic complexity classes, such as the
space and time hierarchy, interactive complexity classes (such as `IP`, and
more vaguely `ZKP`), and circuit complexity.
- [Infosec lecture notes (does not render well)](https://github.com/bollu/subject-notes/blob/master/pois/main.pdf)
- [Complexity theory lecture notes](https://github.com/bollu/subject-notes/blob/master/complexity/main.pdf)
- [Algorithms lecture notes](https://github.com/bollu/subject-notes/blob/master/caa/main.pdf)
# FPGAs
FPGAs (Field programmable gate arrays) are essentially programmable hardware.
That is, they comprise of hardware parts which can be "programmed" to perform
any hardware operation one wants to. So, if you have a very specific operation
in mind, it is potentially way faster to run on an FPGA with dedicated hardware
than running the same thing on a general purpose processor.
The difference between an FPGA and as ASIC is that FPGAs are _way_ cheaper than
manufacturing an ASIC, which is time and money intensive, and is also risky. If one
messses up the hardware programming on an FPGA, we can always reprogram it. On
the other hand, once an ASIC has been "taped out" (as they say), it's a block
of silicon. If it's messed up, then good luck, you just wasted over
a hundred thousand dollars.
However, eventually, ASICs do get cheaper at humongous volumes, so
it's not that `FPGA > ASIC` in every situation.
I've been learning how FPGA's work, due to a course in college. I've been
interested in the inherent reconfigurability of FPGAs. The questions I've had
in this space were:
- How easy/hard is it to design hardware for an FPGA?
- Can we create hardware for pure functional languages (aka, STG on hardware)?
- What kind of languages exist for programming FPGAs? Would a haskell-like language
do well?
##### Answers to the questions
- TL;DR: It's hard.
- We probably can create STG on hardware, since people have done so before.
- None of the current languages meet my taste, so I build one.
The current situation as far as I can see is like this:
- Use a language such as System Verilog, which is poorly designed (in the sense
of C), and leaves way too many low level details / sharp corners for my taste
- Use a language such as BlueSpec verilog, which is proprietary (like most things in this space),
and is _still_ not nice enough for me to consider, because frankly the compiler
produces really cryptic error messages, and debugging it is a real pain. I program
in Haskell, I'm not confused by the purity, or the type strictness of the language.
However, it does take many questionable decisions -- eg, not having an escape
hatch for `IO` to debug, no real introspection possible during the elaboration
portion, etc. But it's by far the nicest thing I've found, which is sad in itself
- Use a DSL embedded into Scala such as Chisel. I haven't tried this one out yet,
but I'm somewhat reluctant, because my experiences with Scala have been unpleasant
so far (`sbt` is slow, the language is... over designed)
- Use `Clash`, a Haskell to FPGA compiler. I dislike this approach, since I think
hacking GHC to produce verilog is a fundamentally strange idea, since I hold
the strong belief that we should _not_ be using turing complete language to
describe anything, much less circuits.
So, I propose my solution: Write a DSL in haskell that leverages all the
nice concepts discovered by haskellers: I'm currently betting on some combination
of applicatives, profunctors, and arrows to provide me with the right abstractions
I need to describe computations on an FPGA in a "natural" style, while still
being _nice to use_.
I think Haskell's arrow syntax does remarkably well with this, and I have
an experiment trying to get this up and running: [`bollu/dataflow`](https://github.com/bollu/dataflow)
# Haskellisms
Learning Coq was a huge boost to doing funky haskell things, such as
playing weird type level games, and getting used to things such as
`ConstraintKinds`, along with general type level programming goodness.
I also read a lot of papers on my to-read pile, including arrows,
update monads, and hyperfunctions. While doing so, I would up adding to the
docs of related packages (such as `ekmett/hyperfunctions`), or writing
expository blog posts of libraries.
## [Arrows](https://github.com/bollu/haskell-koans/blob/master/arrow.hs)
As mentioned in the FPGAs section, arrows were initially created to describe
parsers as a thing that's in-between in terms of power of `Applicative` and
`Monad`. The intuition is that `Arrow`s represent machines / chains of computation /
dataflow.
## [Hyperfunctions](https://github.com/ekmett/hyperfunctions)
I don't really understand these, but they seem to allow one to construct a
`Monad` which provides one the ability to perform diagonalization. I've
added links to the `hyperfunctions` repo that adds the link I wanted to read.
## [Guanxi / Propogators](https://github.com/ekmett/guanxi)
Edward Kmett introduced me to the idea of propogators
([tech report: the art of the propogator](http://web.mit.edu/~axch/www/art.pdf)),
which is an idea I find very appealing. The general framework appears to allow
one to mix different kinds of "solving strategies" (think constraint solving + ILP
+ ...), into a neat framework. Edward has a bunch of stuff on how to use this
framework effectively, but I'm in it as a nice theory of how to write solvers.
### [Structs](https://github.com/bollu/blog/blob/master/content/blog/reading-kmett-structs.md)
The `Guanxi` repo contained references to `structs`, so I wound up writing a blog
post about it. TL;DR - it allows one to create a universe of mutability within
GHC, and provides a nice interface to do this with template haskell.
Click on the title for the blog post where I explore the library.
## [Deltas: An algebraic theory of patches (WIP)](http://github.com/bollu/deltas)
I've always felt that patches / patching should have an algebraic structure,
and I'd initially dismissed it as "yeah, patches form a group action on files,
that's trivial".
I decided that I had to implement this "trivial" idea to be sure, and this
led me down a rabbit hole. There's something really deep going on in the theory
is my feeling, which I've documented on the `README` of the package.
The reason I want such a library is to be able to write compiler passes that
I can cheaply "speculate" on and unroll. This would be really handy to have
in LLVM, since we do a lot of things speculatively, but there's no nice way
to roll back. This motivation was arrived at after long discussions with a
friend, [Philip Pfaffe](https://github.com/pfaffe).
Storing snapshots of the compiler state is _super_ expensive, so we _need_ some
way to make it cheap if it's used at all. It would be amazing if someone could
devise a theory that tells us how to
- Automatically derive the correct choice of a "delta / diff / patch" for a
given type.
- Use the algebraic structure (ie, a group) to simplify / collapse rewrites.
- Use / exploit laziness to make sure that we don't pay for what we don't need,
in terms of applying patches.
The `deltas` package is a way for me to explore solutions in this
design space.
# The philosophy of science
I've always been bothered by my belief in science with no real justification
to back it up. I decided to patch this hole, and hence went about reading
and studying the philosophy of science. The books I read were:
## Proofs and refutations, Imre Lakatos
This book is excellent --- it's structured as a student teacher dialogue,
as they go through building a mathematical proof, and different viewpoints
one can have as one goes through the process of performing mathematical thinking.
It's a pleasure to read, though I suspect I haven't really digested a lot of the
book, it's one I need to re read.
## The structure of scientific revolutions, Thomas Kuhn
This is the book that coined the phrase _paradigm shift_.
## Popper on falsifiability
Popper was the first one to actually construct the notion of what differentiates
science from not-science as falsifiability. There are many fanciful ways of
summarising what falsifability is, but the nicest is to say that:
> every theory must come with a reasonable method to disprove itself
So, for example, relativity made particular predictions about orbits
that deviated from newton's laws. So, if one wanted to prove that relativity were
**false**, one simply had to check that the predictions were wrong!
Another way of looking at this is:
> A scientific theory can never be proved, it can only ever be non-disproved.
This appeals to the [intuitionist]() in me, where `not(not (false)) != true`.
## Paul Feyerabend, against method
This is an amazing book with a really cool viewpoint: The book argues
that "the scientific method" as is carried out in practise is an inherently
anarchic process, which "the scientific method on paper" refuses to capture.
This viewpoint is supported by providing an example of Galileo. When
he proposed the heliocentric model, telescopes were not accurate enough
to determine whether his theory was correct or not. Hence, it's a little
weird that people shifted to heliocentrism, despite not fulfilling the criteria
of the scientific method!
If one buys the argument, then this leads to really interesting places --- for
example, now that we have shown that science in the real world isn't some
"special process" that actually adheres to the supposed scientific method,
why should we trust it? We must perhaps take science as seriously as
we take religion!
I don't buy the argument, since I value science not because scientists follow
the method, but because scientists care about _explaining_ the natural world,
and the ability to predict and explain should be taken seriously.
Even so, it's a great book to see a serious attack on the method itself.
I'd love more suggestions along the lines of this book --- well thought out
responses to the scientific method. (Drop me an email at ``
if you have suggestions, please)
# Linguistics
I have a bunch of friends who are computational linguists, so I've always
been interested in the field. The general list of things I've wanted to read
up was on:
- Word embeddings, since they somehow seem to capture the structure of language
--- perhaps conforming the distributional hypothesis.
- Conlangs, since I find them interesting to look at from an information theory
perspective. I've heard from the linguists (I have no idea how true this is)
that natural languages look very different from languages that a coding theorist
would come up with to transmit information. I've always wanted to understand
why this is, and where the fundamental difference comes from.
For this year, I read some amount of word embeddings literature, particularly,
`Word2Vec`, `GLoVe`, and the `Poincare embeddings` paper. I found them
fascinating, and when I find the time, I plan on experimenting with
different spaces for word embeddings to go into.
# Bedtime reading
I often pick up textbooks which I can skim through right before I sleep. I find
that this is a remarkably good way to pick up a lay of the land, which is
helpful the next time one wants to learn ideas in detail. This year, I did
so with:
## [Rationality, From AI to Zombies](https://intelligence.org/rationality-ai-zombies/)
I was vaguely aware of Elzier Yudowsky and the surrounding rationalism
movement, but I'd never seriously read it.
So, I plonked down and read through all the writings on [Lesswrong](https://www.lesswrong.com/),
a blog dedicated to being "less wrong" when we think about things.
I found it _interesting_, but a lot of it was just rehashing ideas that I
had heard of, or were always around in the environment I grew up with. I
suppose it would make a fine book for converting someone who's undecided
about their positions on topics such as atheism, rationality, science, and
whatnot, but as someone who's already drunk the kool-aid, I didn't find
a huge amount of insight.
Even so, it's a well written and thoughtful collection of blog posts,
so I'd recommend it to everyone.
## [Purely functional data structures, Chris okasaki](https://www.cs.cmu.edu/~rwh/theses/okasaki.pdf)
This is a book that describes the implementation and analysis of data structures
for immutable languages. The short version of the story is that before this
book, we did not know how to analyze immutable data structures, since our arguments
for amortized analysis depend on the "old" version of the data no longer existing.
To combat this, okasaki shows how one can leverage _laziness_ as a tactic to
build data structures that have good _amortized_ bounds on time complexity.
Later in the book, ideas are shown on how to convert _amortized_ bounds to
worst-case bounds.
It's an amazing book, that develops the theory compactly and yet rigorously.
I got a lot out of the book, as well as some _really weird_ facts such as:
- [skew binary numbers](https://en.wikipedia.org/wiki/Skew_binary_number_system), which is a number
system where there is at most one carry on each addition. This lets us define data structures
with `O(1)` `cons` operations, since we learn in the book how to convert number systems
into data structures!
## [Tensor geometry, the geometric viewpoint and its uses](https://www.springer.com/in/book/9783540520184)
This is definitely the coolest book I've read all year, purely for the quotes
at the beginning of each chapter and on the cover of the book. It lifts quotes
from ancient texts of gods, demons, and spirituality, and somehow makes
them fit beautifully into the context of tensor geometry. What this says
about tensor geometry I'm unsure, but it does reflect a deep sense of aesthetics
of the authors that I really appreciated.
They have a penchant for clean notation and geometric thinking, which I absolutely
loved as I read through the book. I'm only on something like chapter 3, but it's
been gorgeous so far and I have no reason to suspect this will change.
For example, the chapter on "Notation" begins with:
>Therefore is the name of it called Babel;
>because the Lord did there confound the language
>of all the earth
The chapter on "Affine spaces" (which are vector spaces where one forgets
the origin) has:
>"Let the thought of the dharmas as all one bring you
>to the So in Itself: thus their origin is forgotten
>and nothing is left to make us pit one against another."
> ~Seng-ts'an
And for one last choice, the chapter on dual spaces has:
>"A duality of what is discriminated takes place in
>spite of the fact that object and subject cannot be defined."
> ~ Lankavatara Sutra
Truly a treat.
# Wrapping up
So, that's been my 2018 in terms of things I've learnt, broadly. I'm sure I've
left out a bunch of stuff that are odds-and-ends, but this covers most
of what I've been hacking on and thinking about.
If you have any suggestions for things you think would be up my alley,
please ping me at ``.
If you liked the blog, star it!