amw-zero

7 ms·

31.
by amw-zero 11mo ago
And to clarify - only writes on the _branch_ lead to a copy being created right? Writes on the original don’t get propagated to the branch?
32.
by amw-zero 11mo ago
What does this even mean? Because people have locked in their data, they’re ok with downtime? I can’t imagine a world where this is true.
33.
by amw-zero 1y ago
The “simplicity” of Go is just virtue signaling. It has gotchas like that all over the language, because it’s not actually simple.
34.
by amw-zero 1y ago
How often are you writing non-trivial data structures?
35.
by amw-zero 1y ago
I love the euphemistic thinking. “We built something that legitimately doesn’t do the thing that we advertise, but when it doesn’t do it we shall deem that hallucination.”
36.
by amw-zero 1y ago
Hard disagree. Errors are found in human proofs all the time. And like everything else, going through the process of formalizing to a machine only increases the clarity and accuracy of what you’re doing.
37.
by amw-zero 1y ago
The first topic is "Predicates, Sets, and Proofs." I use predicates and sets quite often in daily programming.
38.
by amw-zero 1y ago
You can write proofs along with the course, and since they are machine checked you can have confidence that they are correct. If you don't know, writing a proof in isolation can be difficult, since you may be writing on that isn't
39.
by amw-zero 1y ago
Research points to there being a quadratic relationship between automated proof and code size: https://trustworthy.systems/publications/nictaabstracts/Mati... . Specifically, the relationship is between the _specif
40.
Let's All Write Good Software(youtube.com)
2 points by amw-zero 1y ago|0 comments
41.
by amw-zero 1y ago
There are 2 main problems in generative testing: - Input data generation (how do you explore enough of the program's behavior to have confidence that you're test is a good proxy for total correctness) - Correctness statements (how
42.
by amw-zero 1y ago
Are you aware of how many allocations the average program executes in the span of a couple of minutes? Where do you propose all of that memory lives in a way that doesn’t prevent the application from running?
43.
by amw-zero 1y ago
You can write proofs in TLA+ and many other formalisms. You don’t need to ever use a model checker. The proofs hold for an infinite number of infinite-length executions. We are definitely not limited to finite behaviors.
44.
by amw-zero 1y ago
> this doesn't replace the lower level page heap storage So this is wrong. The heap storage is replaced.
45.
by amw-zero 1y ago
How do table access methods work with standard PG concepts such as the shared_buffers cache? Is that irrelevant since data is stored in FDB? Also, how do the deployment semantics of FDB affect this. If I remember correctly, you typically ru
46.
by amw-zero 1y ago
> From what I can tell, this doesn't replace the lower level page heap storage, but instead actually provides new implementation of table and indexes These seem contradictory. If the data is stored in FoundationDB, then it won'
47.
by amw-zero 1y ago
Eh. I like to wing it and call it whatever I like. If the content is good, people will find it.
48.
by amw-zero 1y ago
You’re confusing statistics with forecasting. We can and should trust statistics. We should just never trust their relation to future behavior.
49.
by amw-zero 2y ago
Not all proofs have proof terms, so not all proof can be compiled to existing languages.
50.
by amw-zero 2y ago
We should look at formal verification like everything else: in terms of statistical effectiveness. It's not really important whether or not there are _no_ bugs. What's important is how many bugs there are for each unit of "ef
51.
by amw-zero 2y ago
Yes - that is what [Validation]( https://en.wikipedia.org/wiki/Verification_and_validation ) is for. I'm not saying it's easy (it's not). But there is a term for this.
52.
by amw-zero 2y ago
You are describing "validation": the process of verifying that your spec really says what you mean.
53.
by amw-zero 2y ago
This exactly describes my intuition as well. Language is limited by its representation, and we have to jam so many bits of information into one dimension of text. It works well enough to have a functioning society, but it’s not very precise
54.
by amw-zero 2y ago
Curious. At that scale and transaction rate, are you deleting / offloading rows to another storage solution after some amount of time? I’m assuming you’re not just letting 150,000 rows a second accumulate indefinitely.
55.
by amw-zero 2y ago
I totally agree. Standard ML set the stage for everyone to finally formally specify a full language, and only WebAssembly has carried the torch as far as I know (other than small research languages).
56.
by amw-zero 2y ago
Those are all programming languages.
57.
by amw-zero 2y ago
Throughput is a property of a queue.
58.
by amw-zero 2y ago
Your whole system is a queue. Requests come in, are processed, and some output is given. Algorithmic complexity affects the processing time of each request / task. Knowing the latency distribution is crucial in understanding the queuei
59.
by amw-zero 2y ago
A queue is: * An arrival rate of requests * A processing time for each request * A corresponding queue length when a new request comes in before the current one is done being processed. So anything that affects processing time affects queue
60.
by amw-zero 2y ago
Loved this writeup, because queues are the most important and general concept in reasoning about performance. When you realize this, you start seeing them everywhere. Locks, async IO... everything is just interacting queues.

More ›