153 karma · joined July 11, 2020
For example (https://www.nature.com/articles/s41598-020-72817-7): where NPRF means non-preferred reference frame:
"Herein, we make progress on that front by extending NPRF to include the measurement of another fundamental constant of nature, Planck’s constant h. As Steven Weinberg points out, measuring an electron’s spin via Stern–Gerlach (SG) magnets constitutes the measurement of “a universal constant of nature, Planck’s constant”3, p. 3 (Fig. 1). So if NPRF applies equally here, everyone must measure the same value for Planck’s constant h regardless of their SG magnet orientations relative to the source, which like the light postulate is an empirical fact. By “relative to the source” of a pair of spin-entangled particles, we mean relative “to the vertical in the plane perpendicular to the line of flight of the particles”4, p. 943 (Fig. 2). Here the possible spin outcomes ±ℏ2 represent a fundamental (indivisible) unit of information per Dakic and Brukner’s first axiom in their reconstruction of quantum theory, “An elementary system has the information carrying capacity of at most one bit”5. Thus, different SG magnet orientations relative to the source constitute different “reference frames” in quantum mechanics just as different velocities relative to the source constitute different “reference frames” in special relativity. Since NPRF leads to the counterintuitive aspects (“mysteries”) of time dilation and length contraction in special relativity, it is perhaps not surprising that NPRF produces a “mystery” for quantum mechanics associated with the measurement of h as well."
There is yet room to grow in QM. I definitely agree with the the original paper's argument on how and why the focus has moved away from foundations, and why the Copenhagen interpretation gets more emphasis than it should. Since this is a very hard nut to crack, the human organizational impulse is to shut up and do. And for new comers who can't do, all they can do is verse themselves in Copenhagen so at least they can do that.
https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-...
which gives this example for a distributed lock:
mutex(τ ) := τ = τ1 ++ (n1, Grant) ++ τ2 ++ (n2, Grant) ++ τ3 → (n1, Unlock) ∈ τ2
What this safety requirement means is that if the lock is granted in some pending message to host n2 (say delivered or in queue to be delivered) then it must have been proceeded by an unlock message and not on the same host getting the grant --- in fact on the last node who was granted the lock. Here n1, n2 designate hostIds.
What I like about this approach, is that Verdi seems to make it quite easy to model and specify in terms of nodes, processes on nodes, and messages between nodes whether on a reliable or non-reliable network. And safety conditions seem to naturally flow, in part, from how messages are ordered when sent. Of course, in an unreliable network which Verdi can model too, they may come out of order requiring more work to de-dup and/or ensure exactly-once-delivery.
Point taken. Programmers may see project uncertainly as less pressing/difficult while formal methods are onerous. How much one or the other depends on details, and how the team frames risk and methods to reduce it. Even on the project side, for example, the Chaos report from the 1990s shows some 40% (60% at small companies) of software projects are cancelled before delivering anything mainly due to scope change and lack of executive support. Both require attention. Both are non-trivial.
While we're on formal methods I'd like to solicit your opinion a bit more. I am working on a distributed KV store which I'd like to formally certify. I started with TLA+ except that compared to Dafny, Verdi the gap between spec and implementation is higher. I don't like that. Verdi, in particular, comes with formally verified, shimmable network layers plus the ability to produce runnable code from the Coq spec. My practical assessment is,
+ Dafny: pros: Refine spec to implementation; provides safety and liveness checks. Can produce runnable code towards testing, Q/A experimentation.
- Dafny: cons: The Dafny GIT repo is a mess --- extremely disorganized and therefore hard to simulate examples in papers with the real thing. It's very hard to see what libraries to build on.
+ Verdi: pros: Like Dafy which came after Verdi, it's focused on refinement: go from spec to more and more implementation detail. It's based on Coq proofs and Coq has tons of books, examples, exercises. See https://softwarefoundations.cis.upenn.edu/ for five solid write-ups concluding with formally certified C code. So I do not see Verdi as overly academic. It has formally verified libraries that can be re-used esp. in the area of message passing, marshalling which models reliable and non-reliable packet delivery. Moreover, and this is important for distributed programming, proofs can be done in terms of traces. Not sure if TLA+ and it's model checker TLC can do that.
- Verdi: Cons: I have to learn Coq, not the end of the world but it's another chunk of work. Also Verdi can't help with liveness checks while TLA+ and Dafny or Spin can. I initially worked with SPIN and TLA+: those specs are checked in a model checker which looks for counter examples. I have a certain feel for that. On the other hand as I understand it out the box, Dafny or Verdi or FRAMA-C use proofs. Now a proof is formal and is help, however, I am unclear if Dafny, or Verdi will give me a counter example if a refinement goes wrong. More specifically, if a refinement is wrong which happens: one is unable to prove a claim - and that's your head's up ... or at some point a run of the executables made will assert a violation of a safety property. I'm not sure.
+ TLA is of course much used in industry -- so I won't plough that field again. But I wish I knew if it can prove system properties through traces like Verdi because it seems such a natural way to reason about distributed systems. TLA+ of course does liveness and safety checks.
All of these are free tools ... including SPIN ... so if one can put the time in you can get a lot of power. That's good to know. Navigating some of the finer details as I suggest here is not so easy when choosing one.
For my little project I was thinking Verdi for safety and TLA+ for liveness checks when needed.
Please weight in ... I'd love to hear more perspectives.
While unit testing and what not has it's place there clear advantage of FM is the developer comes up with the spec first then show/prove it rather than coming up with the spec bug by bug by bug which can be slower and more labor intensive and customer facing.
Look if you tell a Dev team we'll need to do four quarters of work over 15 jira epics implemented in two week sprints nobody complains that the plan is dumb because all the requirements aren't really nailed down, the scope could change, or the team might not come up with the algos .. So why even try?
But if you tell the same team we'll be using formal methods there's a lot of complaining because FM can't check everything ... Not down to the real final code ... So why bother? I find this dichotomy disingenuous by programmers.
Can you please clarify? A tla+ spec (or pluscal to tla+) is supposed to verify against all possible interleavings of reachable states like spin. You seem to be saying something different
* one of the major problems at corporations is lack of openness. People BS all the time. Worse, and I've seen several of these in my job, people believe that if you do not manage-up and BS then you're a chump. Part of the management is to cut this BS out. The difference between you and me at this point in time is that it's an unchecked assumption for you, but not for me.
* Cross functional coordination is essential to proper corporate governance. In particular, manager's damn well drill into internal service suppliers they'd better be customer driven and not make whatever they want - see also Conway's law. A lot BS at companies is half-assesd internal suppliers who underperform because they get management cover 'cause we have to use them ... and they cannot be essentially fired without extraordinary cause. Cross functional coordination is essential to getting and keeping people on the same sheet of music.
I'd read "Human Element" (Dr. Schutz) and "Total Quality Management the Japanese Way" (K. Ishikawa [might be sp there but title is good]).
In my experience manufacturing knows this is true, even they don't always practice it. But most service companies are clueless.
Yes, if you don't have a management approach (TQM the Japanese way), you don't have a solid framework to human organizations and teams (Human Element), you don't have cross functional coordination, you don't have customer driven teams, and management tolerates the BS ... then you don't in fact have management and you do have politics whence I refer you to my original statement.
- no more headlines like "what nobody (read power structure) will tell you .. the real story behind..." which sours information by building mistrust. People are wrong, don't know, sometimes right but the entire msm is not people lying to you and you (readers) are not chumps. Let's do better.
- the constant bitching, whining, sniveling by media group 1 about media groups 2, 3, 4... Look you gotta something to say, say it. You can argue the other side got it wrong. Say it. And leave it there. What I don't want to read is third grader stuff: Biden wears a hair piece and. NPR and CNN know it but but wont say anything. Whining about claimed tribes and tribe favoritism isn't a journalist's task. It has the side effect seen in article of making the writer small, powerless, and unequal to the task.
The last issue I believe has its roots (maybe not chronological firs but in impact) to rush Limbaugh who successfully got am into politics by claiming mainstream media plays favorites. Fox later did the same on TV.
----- match item_option { Some(item) => {
//Do something with resource
println!("{}", item);
}
None => {}Wouldn't this be better with design by contract by having first() enforce length>0 then turning off assertions if desired for release code? Also OP should have mentioned not matching none is an error otherwise there's no point
Also software development makes all intelligent actors into mumblers usually after year 7 ... so we can expect to hear, if we strain our ears, some more choice words from Captain SourceCode. Gonna be fun!
- breaking the domain of work into well modeled types
- information hiding
- keeping dependencies together and/or variously keeping data dependencies apart
- leaving room for extensibility
- speed of operations
- and promoting the correct use i.e. single v. multi-threaded or one server vs. distributed
That's real work, and getting a "good API" i.e. recognized throughout industry as well adapted to the problem domain (say SQL for DB work) or copy-on-write for C++-strings almost always reflects a better implementation which bubbles into the API.
You either make your spec up as you go along and don't check it as its hidden in the code, or provide it so that static analysis tools and/or things like tla+ can help confirm. There never was any getting around that regardless of language. The code follows from spec which both follow from requirements
A side comment somewhat in humor is the killer app that's used to explain rete rules engines which is frequent fly programs: how in heck can you compute what a customer is due with all thr crazy rules. This is akin to fica scores for loans and credit cards.
What's a little misleading in the example is that the problem setup already is a half answer. In complex commercial apps just arriving at an apportionment of 5 and .05 for some narrow set of use cases is already an achievement.
If we see 5 and .05 comes in the mixed case (CPU in the i/o loop) then there is a choice on what to fix to drive down absolute time. If the numbers are not so skewed it may take more debugging to suss out what's going on. Here it is obvious with givens.
If apart we conclude the i/o is slow (pedantically i/o bound) and there's no engineering need to figure out where labor needs to go. Here it's pointless to wonder about CPU or memory.
The emphasis in sum is on the management end: our system slow. But what are we going to fix and why.