[HN Gopher] Programming as Theory Building (1985) [pdf]
___________________________________________________________________
Programming as Theory Building (1985) [pdf]
Author : solomonb
Score : 138 points
Date : 2023-08-25 15:51 UTC (1 days ago)
(HTM) web link (algoritmos-iii.github.io)
(TXT) w3m dump (algoritmos-iii.github.io)
| distortionfield wrote:
| This article has probably the most exact description of both
| software engineering as a craft and as a problem set that I've
| yet come across. It perfectly describes that essence of all
| engineering that can only be captured by innate understanding and
| experience as a function of time, and not just "book smarts" for
| lack of a better word. 10/10, great read.
| dang wrote:
| Related:
|
| _Naur on Programming as Theory Building (1985) [pdf]_ -
| https://news.ycombinator.com/item?id=31500174 - May 2022 (4
| comments)
|
| _Naur on Programming as Theory Building (1985) [pdf]_ -
| https://news.ycombinator.com/item?id=30861573 - March 2022 (3
| comments)
|
| _Programming as Theory Building (1985)_ -
| https://news.ycombinator.com/item?id=23375193 - June 2020 (35
| comments)
|
| _Programming as Theory Building (1985) [pdf]_ -
| https://news.ycombinator.com/item?id=20736145 - Aug 2019 (11
| comments)
|
| _Peter Naur - Programming as Theory Building (1985) [pdf]_ -
| https://news.ycombinator.com/item?id=10833278 - Jan 2016 (15
| comments)
|
| _Naur's "Programming as Theory Building" (2011)_ -
| https://news.ycombinator.com/item?id=7491661 - March 2014 (14
| comments)
|
| _Programming as Theory Building (by Naur of BNF)_ -
| https://news.ycombinator.com/item?id=121291 - Feb 2008 (2
| comments)
| brutusborn wrote:
| I think this can be said of any engineering design or even
| designing policy: design is essentially producing hypothesis that
| a design is the 'best' solution of problem where 'best' is
| defined by some method to predict the outcome of the design.
| kaycebasques wrote:
| I went through all the previous HN discussions on the paper. I
| don't think I've ever done that before and don't know what
| compelled me to try today. It was rewarding! Pretty much every
| thread had new ideas not discussed in previous threads.
|
| One quick takeaway: it seems like reading Ryle's _The Concept of
| Mind_ to really understand Naur 's idea of "theory" is a good
| next step for going deeper on this topic.
| slotrans wrote:
| Fantastic paper, possibly THE most important paper on software
| engineering. Unfortunately the language is quite dry and
| academic. This piece commenting on the paper is a nicer read
| https://www.baldurbjarnason.com/2022/theory-building/
| fsloth wrote:
| Agree! It's importance can be grasped only once a person has
| spent some time in organizations with non-trivial amount of
| software to maintain.
|
| After that reading it is like discovering Newton's law of
| gravitation. It'a an abstract model that explains _so much_ of
| what goes wrong in software.
| corethree wrote:
| It's theory building based off of seat of your pants gut
| feelings. If you build a shack haphazardly out of sticks and glue
| that's also "theory building".
|
| 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.
|
| 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'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.
|
| A program designed like this ends up being made up of thousands
| of primitives, most primitives likely used once or twice only.
| Nothing composes.
|
| Technically your still theory building just like how building a
| house out of garbage, straw, glue and tape is theory building.
|
| 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
| "theory" in the way we think of it?
|
| 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 "theory"? Yes. It's
| called algebra. Algebra based designs
|
| Haskell largely facilitates this style of programming.
|
| 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.
|
| Here's a small example of what a "theoretical" program looks
| like:
|
| https://github.com/pyrofolium/parser_combinator_python/blob/...
|
| It's a JSON parser. I started with an axiom: func(string) ->
| Option<tokens, string>
|
| 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.
|
| 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?
|
| As I constructed the parser I constructed the theory which formed
| a base set of parser primitives I could compose to form bigger
| parsers. Biggerparser = smallerparser +
| othersmallerparser
|
| Unlike most custom parsers if you go through this code it's
| somewhat readable.
| crabmusket wrote:
| Nair's use of "theory" in this paper is highly specific and
| instrumental. Section 4 covers it.
| corethree wrote:
| We don't really call "Culinary arts" theory, it's more of a
| "art" Peter is largely not thinking deeply and as a result he
| defines "theory" in such a way that it refers to "Painting
| Portraits" as "theory" and lumps it with "The theory of
| Quantum Mechanics"
|
| Generally we don't refer to "Culinary arts" as theory while
| we do so with "Number theory." A subtle distinction in
| meaning exists in our subconscious and Naur simply didn't
| have the self awareness to see the distinction. That's what
| results in his largely informal and qualitative paper about
| mostly nothing. Yeah building a program about say E-commerce
| is Obviously building knowledge around e-commerce... call it
| "theory" if you want but in essence it's nothing new under
| the sun.
|
| You need to think in terms of the idea of "formal theory."
| Complex Number theory, The theory of general relativity.
| These things are distinctly in the same category as
| "knowledge" but refer to something more precise.
|
| Naur likely felt the distinction but failed to put his finger
| on it. Like many laymen, if you call Scientology a "theory"
| they think of it on the same professional level as the
| "theory of Gravity". It's largely what Peter is doing with
| programming... he's just using the word "theory" to give
| programming more legitimacy.
|
| He's not the only person to do this. Other bullshit like
| "Color theory" which chooses red, yellow and blue as primary
| colors is really just an arbitrary grouping that is only
| called "theory" to give it artificial legitimacy. The color
| sensors in your eyes are actually red, green and blue and
| color itself is actually a gradient of frequencies.
|
| What Naur failed to realize is that Programming is distinctly
| the perfect vehicle for formulating formal theories around
| any subject. Keyword: "formal" Imagine a theory of
| "e-commerce" as formal and rigorous as Newtonian Mechanics.
|
| But we almost never do this as programmers. Instead a program
| is more like "Culinary arts" a patch work of procedures and
| steps with no cohesion.
|
| I made a JSON parser in the link above. And that parser is
| built using formal algebraic theory. The entire parser is
| created as a formula. An equation of smaller parsers.
|
| It is literally the formation of a Formal theory of parsing.
| Or you can think of it as a Formal Algebra of parsing.
|
| Obviously there's a larger theory in academia on parsing. But
| in my program there's a little formal theory there.
|
| If programs are theory building. This is what is should be,
| this is what his paper should have been about. I think this
| was his intent, he just lacked the background to fully
| articulate and realize what is essentially a vague
| equivalence analogy between "programming" and "theory".
|
| Largely readers of the paper and people who agree with him
| fell for the same trope.
| kqr wrote:
| Huh, I accidentally discovered this connection[1] recently and
| found it somewhat powerful. Very nice to hear that someone else
| has written about it -- Peter Naur no less. Thanks for sharing!
|
| [1]: https://two-wrongs.com/abduction-is-not-induction.html
| grumblingdev wrote:
| Very hard to skim over. Can anyone summarize? Looks like its
| trying to make a very simple point in a very long-winded way.
| amw-zero wrote:
| I think you should be able to read a 9 page paper. But here is
| a summary: https://ratfactor.com/papers/naur1.
| 0x445442 wrote:
| Thanks for the link. I really like the bit that expands on
| the notion that premature optimization is not limited to run
| time optimizations but to, perhaps more so, abstraction
| optimizations.
| keithalewis wrote:
| Username checks out.
| fsloth wrote:
| The point is not simple. It's the most perfect summary of the
| biggest problems in software engineering ever written.
|
| There are rare papers that are worth investing time. This is
| one of those.
| dahjelle wrote:
| I gave a talk on it at a local meetup. Here's my notes and
| slides: https://gitlab.com/dahjelle/programming-as-theory-
| building-2...
|
| The Future of Coding podcast also had an episode on it:
| https://futureofcoding.org/episodes/061
| crabmusket wrote:
| That FoC episode was my introduction to the show and was
| completely fantastic. The discussion was interesting, but
| they also had a lot of fun with the format which I was not
| expecting.
| layer8 wrote:
| Read the conclusion at the end of the paper, it's a single
| paragraph.
| ryandv wrote:
| The most difficult and time consuming activity of software
| engineering is not the production of source code as a textual
| artifact, but building a mental model of the software system -
| why it was built a certain way, how it may be extended, how it
| may not be extended, how to answer questions about the system,
| an understanding of the abstractions within it and how to use
| them. In particular, this understanding exists outside of the
| source code itself.
|
| It's for this reason that I am skeptical of ChatGPT, which
| automates the most trivial part of software engineering -
| writing the code. GPT will not give you understanding, only the
| textual artifact (and whether or not this artifact is actually
| the product of some AI "understanding" is unclear).
| tudorw wrote:
| While the underlying model may not have 'understanding', the
| iterative process of interacting with the model creates a
| context that in my experience has captured part of the 'area
| of interest' during a pair programming session, our
| interactions have created a unique context that means the
| model responds as if it has modelled an 'understanding', it
| is something more than simply a text record of our
| conversation.
| grumblingdev wrote:
| > for this reason that I am skeptical of ChatGPT
|
| Me too! I think its wayyy over-hyped. The biggest challenges
| in software are architecture. Object boundaries. System
| composition.
|
| And I'm a big believer that all the software we write today
| is shit. So GPT is just regurgitating bad practices.
| fasterik wrote:
| I think this is true for any domain of knowledge in
| ChatGPT. Its knowledge is shallow in a certain sense, but a
| lot of things don't require deep knowledge. Shallow
| knowledge generated very quickly can still be useful.
|
| I find ChatGPT to be very useful as a source of
| documentation. I can ask it to summarize a certain
| scientific topic for me, or how to do a certain thing in
| the Win32 API. I'm not going to take its output at face
| value, but it still speeds up the process of figuring out
| what I should research further, what function to call, etc.
| kaycebasques wrote:
| > Shallow knowledge generated very quickly can still be
| useful.
|
| A great, concise summary of the idea I was grasping at.
| Thank you.
| lordnacho wrote:
| I find it incredible that every time I have a bit of experience
| with something, I find someone a long time ago has already
| distilled the essence down and written an elegant summary, with
| even more detail than I had considered.
|
| This time published within walking distance of where I was living
| at the time.
| impulsivepuppet wrote:
| A strongly-related topic would be Curry-Howard correspondence,
| that is to say that programs and mathematical proofs have a lot
| in common. Proving an assertion is chaining transformations,
| without managing some underlying state / side-effects.
|
| Big difference is that concepts in Mathematics are very immutable
| -- it's unlikely for us to redefine what Euclidean Space is and
| if we find some other framework to be more useful, we'd rather
| give it a new name. I am inclined to say it's a difference in
| discipline and conventions and in the scope and span. Programmers
| will create more when Mathematicians will try to cram their
| discovery into an already packed library, rather than open a new
| one -- the latter happens by accident in the world of Maths.
|
| The workplace of a programmer differs in such a way that a lot
| more mutation (codebase, not just variables) is going on, the
| work isn't purely novel, e.g. will contain mundane parts [2].
| Also, contractual obligation is different from formalism and it
| does appear that programmers work in strictly formal environment
| to achieve goals while mathematicians have goals and vibe but
| have to become correct machinelike interpreters and conjure up a
| formally valid extension on the basis of accepted assumptions.
| Furthermore, there is a disconnect and reconsiliation between
| code and processes, because code resides on layers of
| abstraction. Mathematicians work more cleanly with abstraction
| because immutability allows you to do so.
|
| Programming does toy with pragmatism because the assumption is
| that problems can only be discovered once a prototype is made --
| an earlier version of code is the instrument that enables deeper
| insight and understanding of the underlying project. Math has a
| weird "human brain fetish" that's a bit difficult for me to
| articulate.
|
| Those would be my 2cc to this discussion. I think the overall
| picture has become more clear about what programming and 'theory
| building' is, comapred to the 80s. As computation "broke off"
| from Math and had to reconsile with physics a bit, it's starting
| to enrich the parent discipline a lot more by providing avenues
| and interesting fields of research.
|
| [1]:
| https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
|
| [2]: writing LaTeX and verifying would be mundane but it isn't
| doing maths per se as one could get away with handwritten text,
| unlike programmers having to ultimately compile their code into
| binary and making sure all env variables are set up correctly.
___________________________________________________________________
(page generated 2023-08-26 23:01 UTC)