1. 11

  2. 4

    I recently read this paper for the first time, and really enjoyed it. This summarizing quote at the end is particularly good

    Program construction consists of a sequence of refinement steps. In each step a given task is broken up into a number of subtask. Each refinement in the description of a task may be accompanied by a refinement of the description of the data which constitute the means of communication between the subtasks. Refinement of the description of program and data structures should proceed in parallel.

    There are a few errors in the OCR (or manual transcription?) that produced this document, so here’s a scanned PDF.

    Also see this related paper that conceptualizes software design as a series of transformations on a spec into an implementation.

    1. 2

      Thanks for sharing!

      Also see this related paper that conceptualizes software design as a series of transformations on a spec into an implementation.

      This is something I’m very interested in. In order for this to work correctly, though, the specification needs to be a mathematical implementation of sorts. I like the way Lamber Meertens describes the concept in his 1986 paper on “Algorithmics”.

      It’s still early days in the design and implementation, but I’m hoping to provide first-class support for these kinds of program transformations in the programming language I’m designing. It would be incredible to have a language that fully spans from high level prototyping, for writing specifications, down to low-level optimization, for achieving peak performance.

      1. 3

        Hey, I know that guy! :)

        In fact, I worked at the Kestrel Institute (https://kestrel.edu) ~20 years ago where he was a researcher. They had built a very impressive program synthesis toolkit that aimed to let you do refinement for a category-theoretic model of your problem domain down to running code, with a theorem prover wired up to check your work along the way. The “intermediate representation” between the categorical model and actual hardware was Common Lisp, so there was a lot of opportunity for localized optimization. There wasn’t a rigorous model for thr entirety of that language, sadly, so you kind of broke the chain of formal logic once you dropped down to that level. C and Java code generators came later, but AFAIK the bootstrapping code never moved away CL. (The language was self-hosting once you had the environment up but you couldn’t exactly get to network sockets and other useful but messy imperative stuff without the CL utility libs.)

        I was very much not anywhere near their level when it came for formal methods (or CS in general); my job was basically building internal tools, websites, and packaged versions of the toolkit for distribution on “uninteresting” platforms like Windows and (very newly, at the time) OS X. It was definitely fun to sit around the lunch table with that crew and just soak up the conversation, even when I couldn’t meaningfully contribute.

        1. 2

          Your language sounds like an exciting project 🙂 Thanks for the paper, I’ll add it to my reading list.

      Stories with similar links:

      1. Program Development by Stepwise Refinement (1971) via pushcx 6 years ago | 1 point | no comments