Viewing profile — 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", …

> 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 th…

> 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 t…

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, …

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 …

> 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 ev…

> 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 suppo…

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 th…

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 \ -ldfla…

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 th…

> 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…

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 …

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 Normingt…

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 …

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). T…

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 …

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 sk…

> 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 mea…

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 steal…

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 co…