Programming as Theory Building (1985) [pdf]
It&#x27;s theory building based off of seat of your pants gut feelings. If you build a shack haphazardly out of sticks and glue that&#x27;s also &quot;theory building&quot;.<p>If you want to build something like number theory or a mathematical theory then you need to start your program with axioms and rules. Then from there compose your axioms via the rules to form the rest of your program. Your program should entirely be a composition of well thought out primitives.<p>Unfortunately almost nobody does this. Rather then create a small set of axiomatic primitives to compose most people just add primitives at will to fix something. They don&#x27;t think about how it will compose they just see a problem and shove in a new axiom or even modify existing primitives to make everything work until they get this ugly mess of a monster.<p>A program designed like this ends up being made up of thousands of primitives, most primitives likely used once or twice only. Nothing composes.<p>Technically your still theory building just like how building a house out of garbage, straw, glue and tape is theory building.<p>But thinking this way and to build programs as layered well structured  lego blocks that compose is hard. What can help us think this way? How do you make your programs more closer to a &quot;theory&quot; in the way we think of it?<p>Is there a theory of theories that govern how primitives should compose that will help us think and actually construct programs that are more inline with what we think of &quot;theory&quot;? Yes. It&#x27;s called algebra. Algebra based designs<p>Haskell largely facilitates this style of programming.<p>More then that the fundamental primitive of computing itself a function that takes data and processes that data to form new data in itself forms a composable algebra. Constructing logic as a composition of pure functions forms the basis of the algebra of computing then you use that framework to manipulate other algebras you designed and that ends up as a theory that looks like an actual theory.<p>Here&#x27;s a small example of what a &quot;theoretical&quot; program looks like:<p><a href="https:&#x2F;&#x2F;github.com&#x2F;pyrofolium&#x2F;parser_combinator_python&#x2F;blob&#x2F;master&#x2F;main.py">https:&#x2F;&#x2F;github.com&#x2F;pyrofolium&#x2F;parser_combinator_python&#x2F;blob&#x2F;...</a><p>It&#x27;s a JSON parser. I started with an axiom: func(string) -&gt; Option&lt;tokens, string&gt;<p>Parsers in essence are functions that take in strings and parse part of that string to output some tokens and the remaining unparsed string. It might return an error too. That is the axiom.<p>From here I built a theory of parsing. How do parsers compose to form bigger parsers? What fundamental set of primitives do I need to build a JSON parser as a composition of simpler parsers?<p>As I constructed the parser I constructed the theory which formed a base set of parser primitives I could compose to form bigger parsers.<p><pre><code>   Biggerparser = smallerparser + othersmallerparser
</code></pre>
Unlike most custom parsers if you go through this code it&#x27;s somewhat readable.