stevan

5 ms·

1.
by stevan 11mo ago
> 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
2.
by stevan 11mo ago
> 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 fac
3.
by stevan 11mo ago
> 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
4.
by stevan 1y ago
This post https://jacquesheunis.com/post/bounded-random/ from 2021 contains some newer techniques.
5.
by stevan 1y ago
> 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 be
6.
by stevan 2y ago
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-im
7.
by stevan 3y ago
> 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 lan
8.
by stevan 3y ago
> 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 cappe
9.
by stevan 3y ago
I give two examples of a stateful upgrade in Erlang/OTP in the motivation, neither rely on distributed storage.
10.
by stevan 3y ago
> 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
11.
by stevan 3y ago
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]:
12.
by stevan 4y ago
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 c
13.
by stevan 4y ago
> 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 t
14.
by stevan 4y ago
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.
15.
by stevan 4y ago
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:
16.
by stevan 4y ago
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
17.
by stevan 4y ago
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
18.
by stevan 4y ago
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 thous
19.
by stevan 4y ago
Fixed, thanks!
20.
by stevan 4y ago
> 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 tow
21.
by stevan 4y ago
> 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 n
22.
by stevan 4y ago
Do I understand you correctly in that you'd like more structure? E.g. that you can only deploy an `application` (= supervisor tree)?
23.
by stevan 4y ago
> 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 behav
24.
by stevan 4y ago
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 produce
25.
Erlang's not about lightweight processes and message passing(github.com)
543 points by stevan 4y ago|274 comments
26.
by stevan 4y ago
> 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) y
27.
by stevan 4y ago
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
28.
by stevan 6y ago
Does anyone know of any applications of statistical techniques, like the ones in the handbook, to software engineering in general or testing in particular?
29.
by stevan 6y ago
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
30.
by stevan 11y ago
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 lis

More ›