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.”

I found the 128KB interesting. It reminds me of Forth here you are forced to fit your code in blocks (1024 chars or 16 lines on 64 characters).

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)

Chuck re-implemented the his Forth many times, in fact Forth’s design seems to be centered around being easily re-implementable on new hardware (this was back when new CPUs had new instruction sets). Another example is Chuck’s OKAD, VLSI design tools, to which he comments:

    “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.”

Something I’m curious about is: what would tools and processes that encourage the "Theory Building View" look like?

[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"

[0]: https://www.arp242.net/static-go.html

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.