stevan

That is basically the same as "Proof by reflection" as used by Gonthier, where the Coq kernel acts as the (unverified) rewriting engine.

I don't think it's "basically the same", because this application of the rewrite rules in a LCF-like system is explicit (i.e. the proof checking work grows with the size of the problem), while in proof by reflection in a type theory it happens implicitly because the "rewriting" happens as part of reduction and makes use of with the definitional equality of the system?

For small and medium examples this probably doesn't matter, but I would think that for something like the four colour theorem it would.

Proof by reflection is accomplished by running some arbitrary program during proof checking that has been proven to only return a "true" result if the goal is true. You can do the exact same thing in an LCF system, and in fact that's arguably what a complex LCF "tactic" amounts to in the first place.

I think the difference is that in a type theory you can prove the soundness of the decision procedure to be correct within the system?

From "Metatheory and Reflection in Theorem Proving: A Survey and Critique" by John Harrison, 1995:

"No work on reflection has actually been done in HOL, but Slind (1992) has made some interesting proposals. His approach is distinguished from those considered previously in two important respects. First, he focuses on proving properties of programs written in Standard ML using the formal semantics to be found in Milner, Tofte, and Harper (1990). This contrasts with the other approaches we have examined, where the final jump from an abstract function inside the logic to a concrete implementation in a serious programming language which appears to correspond to it is a glaring leap of faith. [...]"

Proving that your LCF-like tactics are sounds using the (informal) semantics of the tactic language (ML) seems cumbersome.

Furthermore I believe proof by reflection crucially relies on computation happening at the logical level in order to minimise proof checking. Harrison concludes:

"Nevertheless it is not clear that reflection’s practical utility has yet been convincingly demonstrated."

This was from 1995, so fair enough, but Paulson should be aware of Gonthier's work, which makes me wonder if anything changed since then?

But people have regularly asked why Isabelle dispenses with proof objects. The two questions are essentially the same, because proof objects are intrinsic to all the usual type theories. They are also completely unnecessary and a huge waste of space.

I believe proof by reflection relies on proof objects? Georges Gonthier's proof of the four-colour theorem crucially uses proof by reflection.

This post https://jacquesheunis.com/post/bounded-random/ from 2021 contains some newer techniques.

Warp is a high-performance HTTP server library written in Haskell, a purely functional programming language. Both Yesod, a web application framework, and mighty, an HTTP server, are implemented over Warp. According to our throughput benchmark, mighty provides performance on a par with nginx.

Source: https://aosabook.org/en/posa/warp.html

It seems to me that one consequence of the "Theory Building View" is that: instead of focusing on delivering the artifact or the documentation of said artifact, one should instead focus on documenting how the artifact can be re-implemented by somebody else. Or in other words optimise for "revival" of a "dead" programs.

This seems especially relevant in open source, or in blog posts / papers, where we rarely have teams which continuously transfer theories to newcomers. Focusing on documenting "how it works under the hood" and helping others re-implement your ideas also seems more useful to break silos between programming language communities.

For example a blog post that introduces some library in some programming language and only explains how to use its API to solve some concrete problems is of little use to programmers that use other programming languages, compared to a post which would explain how the library works on a level where other programmers could build a theory and re-implement it themselves in their language of choice.

I also feel like there's a connection between the "Theory Building View" and the people that encourage rewriting your software. For example in the following interview[0] Joe Armstrong explains that he often wrote a piece of code and the next day he threw it away and rewrote it from scratch. Perhaps this has to do with the fact that after your first iteration, you've a better theory and therefore in a better position to implement it in a better way?

I also believe there's some connection to program size here. In the early days of Erlang it was possible to do a total rewrite of the whole language in less than a week. New language features were added in one work session, if you couldn’t get the idea out of your brain and code it up in that time then you didn’t do it, Joe explained[1] (17:10).

In a later talk[2] he elaborated saying:

    “We need to break systems down into small understandable components with message passing between them and with contracts describing whats going on between them so we can understand them, otherwise we just won’t be able to make software that works. I think the limit of human understandability is something like 128KB of code in any language. So we really need to box things down into small units of computation and formally verify them and the protocols in particular.”

Speaking of Forth, Chuck Moore also appears to be a rewriter. He said[3] something in similar:

    “Instead of being rewritten, software has features added. And becomes more complex. So complex that no one dares change it, or improve it, for fear of unintended consequences. But adding to it seems relatively safe. We need dedicated programmers who commit their careers to single applications. Rewriting them over and over until they’re perfect.” (2009)

    “I’ve spent more time with it that any other; have re-written it multiple times; and carried it to a satisfying level of maturity.”

[0] https://vimeo.com/1344065#t=8m30s

[1] https://dl.acm.org/action/downloadSupplement?doi=10.1145%2F1...

[2] https://youtu.be/rQIE22e0cW8?t=3492

[3] https://www.red-gate.com/simple-talk/opinion/geek-of-the-wee...

I’ve seen people regularly struggle to write code that accepts all back compat state + handles it correctly.

From the post:

In a world where software systems are expected to evolve over time, wouldn’t it be neat if programming languages provided some notion of upgrade and could typecheck our code across versions, as opposed to merely typechecking a version of the code in isolation from the next?

if you have long running sessions and do several upgrades, are you running N versions of the code & eating up RAM because the old sessions aren’t complete?

I believe Erlang supports two versions running along each other. They capped it at two because back when this was developed there wasn't enough RAM. Joe Armstrong gave at least one talk where he says if he'd have liked to support arbitrary number of versions and garbage collect them as old sessions complete.

Thus I stand by that there’s no “generic” solution you can bolt onto an arbitrary language.

The main point of the post is centered around Barbara Liskov saying "maybe we need languages that are a little bit more complete now". I'm not interested in the limitations of current languages, I'm interested in the future possibilities.

I give two examples of a stateful upgrade in Erlang/OTP in the motivation, neither rely on distributed storage.

This seems like a problem you can’t solve generically and you always end up making trade offs.

That shouldn't stop us from solving the problem in the cases where it's possible though? We can tackle the corner cases separately with manual overrides.

This is probably a big reason why most programs use external storage solutions even if they’re less efficient - it centralizes maintenance of state onto a system that has well defined semantics and can handle repair transparently.

This is certainly the case today, what I'm asking is: does it always have to be like that in the future?

The following post [0] describes how to build static binaries even with cgo enabled:

    GOOS= GOARCH= CGO_ENABLED=1 go build \
      -tags osusergo,netgo,sqlite_omit_load_extension \
      -ldflags="-extldflags=-static"

Not exactly about that? It's literally the example from the motivation. The first thing I do in the plan section is to say "Let's focus on a single stage of the pipeline to make things easier for ourselves." and in the contributing section "We've only looked at one stage in a pipeline, what happens if we have multiple stages? is it enough to control each individual stage separately or do we need more global control?".

The only other place where I see this is useful is competing tasks. One task needs more resources from a thread pool shared by other tasks. A pid controller can allocate existing threads based off of pressure. Allocating more threads to a pool in this case though, still doesn't make sense.

Imagine you got 16 CPUs/cores and a 4 stage pipeline, lets say we want to run one thread per CPU/core for max performance (avoiding context switching). Without knowing anything about the workload: what is the best way to distributed the threads over the stages? You can't tell. Even if you tested all the possilble ways to spread out the threads over the different stages on some particular workload, then as the workload changes you wouldn't have optimal allocation anymore. A controller can adjust the threads per stage until it finds the optimal allocation for the current workload and change it as it changes.

I did take a control theory class in 2009, but I forgot most of it because I never used it.

Nevertheless I did my best explaining what I can, but if you think you can improve upon it then I'm happy to accept pull requests.

There are be plenty of university level textbooks on control theory. For how to apply control theory to software problems there seems to be much less material though. Glyn Normington recommended the following book in another comment thread:

    Feedback Control for Computer Systems
    Philipp K. Janert
    330 pages
    O’Reilly (2013)
    ISBN: 978-1449361693

Good question! At first I thought that maybe I wasn't waiting long enough after the load generator finished, but I just ran an experiment with a longer pause and I still don't see a scaling down after the traffic stops!

Perhaps my naive implementation of the PID controller isn't good enough, maybe:

you'll probably want to put a maximum on your integral accumulator

is needed as icegreentea2 pointed out.

I got the idea of scaling thread pools from a paper[0] coauthored by Eric Brewer (of CAP theorem fame and also vice-president of infrastructure at Google according to Wikipedia). The paper was written in 2001, so things might have changed a bit, but I doubt the example is completely irrelevant today.

[0] https://people.eecs.berkeley.edu/~brewer/papers/SEDA-sosp.pd...

In the 70s Ericsson programmed their telephone switches in a proprietary language called PLEX. It had hot code swapping, so when Joe Armstrong started working on Erlang to replace PLEX in the 80s this was a requirement. Dropping a few thousands of calls just to do an update simply wasn't an option.

Fixed, thanks!

There's a component that seems to be missing here which is preemptive task scheduling.

For Erlang, yes. For implementing behaviours (the point of my post), I don't think so (I sketch a "single threaded" solution towards the end).

I think one worker behaviour per CPU/core per stage in the processing pipeline is better than throwing thousands of processes at the problem and let the scheduler deal with it. This is what I got from Martin Thompson's talks (I linked to one of them in the "see also" section).

To some extent I know... but to some extent the answer is these things are all tied together. Erlang is a really tight ball of solutions to its own problems at times. I don't mean that in a bad way, but it all works together. It needs "behaviors" because it didn't have any of the other things I mentioned.

I can see why you would say that regarding the supervisor behaviour, but I don't see how your argument applies to the other five behaviours I wrote about. Let's keep it simple and focus on, say, `gen_server`?

This is a case of what I'm talking about. Don't confuse Erlang's particular solution for being the only possible solution.

I'm not, in fact I mention that I've started working on a small prototype to explore implementing behaviours in a different way at the end of the post.

Erlang's behaviors are basically the Template pattern (https://en.wikipedia.org/wiki/Template_method_pattern ) written into the language rather than implemented through objects. If you look for the exact Erlang behaviors out in the wild, you won't hardly find anything. If you look for things that solve the same problems, there's tons of them.

My understanding of Joe's thesis is that we can compose a small set of behaviours into complex systems. He and OTP expose and highlight this structure. I don't doubt that other's have also discovered the usefulness of this structure, but I don't see anyone else try to help bring that structure to the forefront so that we can improve the state of software.

Your argument seems to be that this structure has now become implicit in the tools that have been developed since then, but I think again this misses the point: the structure is simple and should be made explicit not hidden away behind 500k lines of C (systemd) or almost 4M lines of Go (kubernetes).

Do I understand you correctly in that you'd like more structure? E.g. that you can only deploy an `application` (= supervisor tree)?

In the light of this statement, the answer to what I think is the thesis question of that entire piece:

"This begs the question: why aren't language and library designers stealing the structure behind Erlang's behaviours, rather than copying the ideas of lightweight processes and message passing?"

[...]

But for the world we live in today, that's a price not worth paying. We don't need the Erlang message bus to be the only message bus. The Erlang message bus is, frankly, not very good, and it's actively terrible if you want to use it for one non-Erlang process to communicate to another. We don't need the Erlang message bus. We have a dozen message busses, some in the cloud, some commercial, some open source, some that double as retention (Kafka), all of which scale better, none of which tie you to Erlang's funky data types.

I asked why they were not stealing the structure of behind Erlang's behaviours, I didn't suggest anyone should steal Erlang's message bus or anything else.

And then, within the matrix of those message busses, we don't need Erlang's restart capability. We have an abundance of ways to restart processes, from systemd, to kubernetes, to any number of other ways.

I don't think restarting the process from systemd or kubernetes is comparable with a supervisor tree. First of all the tree gives you a way to structure and control the restarts, e.g. frequently failing processes should be further down the tree or they will cause their sister nodes to get restarted etc. The other obvious difference is speed.

We don't need Erlang's behaviors. We have interfaces, traits, [...]

Yet I don't know of any other language which uses interfaces in a way which they achieve the benefits (listed in the article) that behaviours in Erlang (e.g. gen_server) give you, do you?

From Joe Armstrong's thesis (p. 6):

In February 1998 Erlang was banned for new product development within Ericsson—the main reason for the ban was that Ericsson wanted to be a consumer of sodware technologies rather than a producer.

From Bjarne Däcker's thesis (2000, p. 37):

In February 1998, Erlang was banned within Ericsson Radio AB (ERA) for new product projects aimed for external customers because: “The selection of an implementation language implies a more long-term commitment than selection of processors and OS, due to the longer life cycle of implemented products. Use of a proprietary language, implies a continued effort to maintain and further develop the support and the development environment. It further implies that we cannot easily benefit from, and find synergy with, the evolution following the large scale deployment of globally used languages.” [Ri98]

I could be misunderstanding you, but this does not sound functional to me as `spec` seems to have access to previous inputs to `spec` invocations. What am I missing here?

In a stateful system (where outputs depend on previous inputs) you need to have access to all previous inputs in order to determine the output of some input, right? Also keep in mind that this is a specification, not an efficient implementation. If you'd implement it like this you'd have to recompute the output based on the inputs over and over again for each new input. And yeah, you can think of it as some kind of functional composition as nine_k pointed out.

This sounds very similar to DDD (like as described as the DDD book at the end of the blog post).

Yeah, I think DDD gets this right: some lightweight methods (e.g. event storming) around inputs and outputs. But yeah, Cleanroom did this in the 80s.

At IBM direct, or are there any particular resources you can point to which you found useful?

On this particular topic, see Harlan Mills' "Stepwise Refinement and Verification in Box-Structured Systems" (1988): https://trace.tennessee.edu/utk_harlan/16/

I like to think of it as "application-as-functional-specification".

A functional specification for a stateful system is a function from a list of all inputs to an output, i.e. `fun spec(inputs: List(Input)): Output`.

This kind of specification doesn't need to specify `State` at all, as we can simply refer to previous inputs. E.g. imagine a counter system with the inputs `Increment`, `Reset`, and `Get`. The functional spec for `Get` is "find the latest reset and then count the number of `Increment`s since then".

I think this is neat, because if you are developing the functional spec with a domain expert that doesn't know programming you don't wanna bother them with, for them, unnecessary bookkeeping details.

From this spec you can then figure out what `State` needs to be, but this can be done as a separate step not involving the domain expert but rather other developers.

I learnt this from the Cleanroom software engineering people, they call the spec without `State` a "black box spec", while the one with `State` is called a "state box spec". (There's also a third step called "clear box spec" where they break down the "state box spec" into functions.)

I've been playing around with the idea of designing a specification language that lets you write "black box specs" together with some basic sanity checks of those specs, because I think there's a lot of value in this sort of structure.

For example even if your application doesn't follow the "application-as-function" pattern, you can still use your "state box spec" as an oracle when doing property-based testing of your application.

Does anyone know of any applications of statistical techniques, like the ones in the handbook, to software engineering in general or testing in particular?

One part that interests me is the discussion about simulation testing in "4.3.3. FEEDBACK THROUGH MONITORING AND SIMULATION" (p. 31 in the PDF).

Alan Perlis says:

  "I'd like to read three sentences to close this issue.
  
    1. A software system can best be designed if the testing is interlaced with
       the designing instead of being used after the design.
  
    2. A simulation which matches the requirements contains the control which
       organizes the design of the system.
  
    3. Through successive repetitions of this process of interlaced testing and
       design the model ultimately becomes the software system itself. I think
       that it is the key of the approach that has been suggested, that there is
       no such question as testing things after the fact with simulation models,
       but that in effect the testing and the replacement of simulations with
       modules that are deeper and more detailed goes on with the simulation
       model controlling, as it were, the place and order in which these things
       are done."

It seems that simulation testing only recently resurfaced with Will Wilson's 2014 Strange Loop talk about how FoundationDB is tested. In fact they seems to have done exactly what Alan Perlis said in 1968, but they never mention any source of inspiration/prior work. Was the technique independently rediscovered, or had they in fact read the (in)famous 1968 NATO software engineering report?

I'd disagree with the two statements:

People who think they understand something about the theory of programming languages, including me, tend to agree that what Python does is wrong.

In fact you can program heterogeneous lists in dependently typed languages, but it’s unreasonably complicated.

Here's some Agda code that shows that both heterogeneous if statements and lists make sense and are easy to work with in type theory.

    data Bool : Set where
      true false : Bool

    if : ∀ {ℓ} {P : Bool → Set ℓ} (b : Bool) → P true → P false → P b
    if true  t f = t
    if false t f = f

    postulate Char : Set
    {-# BUILTIN CHAR Char #-}

    data ℕ : Set where
      zero : ℕ
      suc  : ℕ → ℕ

    {-# BUILTIN NATURAL ℕ #-}

    ex₁ : ℕ
    ex₁ = if {P = λ b → if b ℕ Char} true 0 'a'

    infixr 5 _∷_

    data List {a} (A : Set a) : Set a where
      []  : List A
      _∷_ : A → List A → List A

    data HList : List Set → Set where
      []  : HList []
      _∷_ : ∀ {A As} → A → HList As → HList (A ∷ As)

    ex₂ : HList (ℕ ∷ Char ∷ (ℕ → ℕ) ∷ [])
    ex₂ = 1 ∷ 'a' ∷ suc ∷ []

Lightweight alternatives (to heavyweight Chrome and Firefox):

xxxterm; http://www.peereboom.us/xxxterm/html/

uzbl; http://uzbl.org/

surf; http://surf.suckless.org/

vimprobable2; http://www.vimprobable.org/