“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.”
“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.”
GOOS= GOARCH= CGO_ENABLED=1 go build \
-tags osusergo,netgo,sqlite_omit_load_extension \
-ldflags="-extldflags=-static"
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.