Recommending Griffith to study quantum mechanics is just plain wrong. It's inconsistent, have many gaps in the material. There's a book superior in many regards to Griffith
- the "Quantum Mechanics: Concepts and Applications" by Zettili.
For more advanced topics, this is an amazing book that covers many graduate topics in a unified and consistent notation: https://www.amazon.ca/dp/0691159025
There is recent research on photons (rather than bouncing oil droplets) that backs up the Bohmian interpretation. "Experimental nonlocal and surreal Bohmian trajectories" http://advances.sciencemag.org/content/2/2/e1501466
I am not sure if the different QM interpretations are only a matter of taste in terms of all predictions. These surreal trajectories are seen as nonsense under the Copenhagen interpretation.
I haven't read this paper yet, but I'm a fan of many things published by NIST. If you're a software engineer I'd suggest browsing their website [0]. They have a lot of great high quality content freely available.
They run the US stations for (almost? not 100% sure) everything related to time-keeping [1] [2].
In particular I've found many of their publications on identity management and authN / authZ very helpful in helping me understand the needs of the enterprise. They have some great primers on role-based access control [3] with examples of some of the different kinds of edge-cases one runs into and how they can be solved. It's far too common to read an explanation that just tells you: you can do whatever you want! When you're getting started in a domain it can be incredibly helpful to know how others solved the same problems.
Here's the publication link [4] on the NIST website. I was going to say that I thought it'd be better to link there so people could read the abstract without having to download the full PDF... But I just checked and the website and all its resources weight in over 1MB while the PDF is around 0.77MB. The state we're in is quite unfortunate; I remember their older website being quite nice and fast.
Abstract:
Blockchains are tamper evident and tamper resistant digital ledgers implemented in a distributed fashion (i.e., without a central repository) and usually without a central authority (i.e., a bank, company, or government). At their basic level, they enable a community of users to record transactions in a shared ledger within that community, such that under normal operation of the blockchain network no transaction can be changed once published. This document provides a high-level technical overview of blockchain technology. It discusses its application to cryptocurrency in depth, but also shows its broader applications. The purpose is to help readers understand how blockchain technology works, so that they can be applied to technology problems.
Aside from it's primary benefit of making access possible, one of the really nice things about it is that it uses open standards (regular unauthenticated HTTP, DOIs, no clever js obfuscation). This means that whenever you're searching for a paper and see a DOI, you can do something like:
The weirdest result might be that a pathology that one would ascribe to the empathizing side, borderline personality disorder (BPD), actually positively correlates with measures of systemizing, so there is a strange overlap between BPD and autism, the pathology one associates with systemizing:
More reliable and pronounced sex differences have been found on a similar scale, namely interest in things vs interest in people and that has also been linked to the gender gap in STEM:
Interestingly, some sex differences in cognitive processing disappear when one simply changes the domain to be more focused on people (e.g. rotation of dolls vs rotation of abstract shapes):
So the underlying difference here might simply be in innate preferences to process information that is in a social context vs an arbitrary context.
Autists have a lower preference for the social context, which is essentially a difference in value function, so value from epistemic/predictive accuracy independent of norms gets more weight.
It looks like systemizing emerges in both extremes of the people vs things dimension (though more likely in the latter), explaining both the NCBI study above and the Nature article linked here. Looking only at interest in people is a cleaner approach IMO (not a cognitive scientist though, so take this with a grain of salt). Systemizing seems to basically capture something like abstract thinking, but, guess what, you can also think abstractly about social problems. The crucial point is rather whether it actually feels pleasurable to delve into extremely obscure worlds of symbols and concepts, far removed from ordinary social experience and norms, and here the sex difference is quite pronounced (about one standard deviation). Notably this sex difference appears to be fully determined by presence of prenatal androgen (a male sex hormone such as testosterone), and a preference for gendered toys (dolls vs cars) also been found in some primate species:
It's actually very well defined (or which part are you confused by). I'm stating these things informally as a formal treatment is right now beyond me and it also doesn't really exist. Look up Chu spaces esp their relationship to linear logic. This paper is pretty informative
Linear logic is the shit. I've been reading up a lot on linear logic and certain things I have a hunch it closely corresponds to and I'm convinced it's the formalism for 21st century.
Basically, it's like classical logic but with two players. From player 1's point of view, player 2's AND has different semantics than his own AND.
It's the logic of state developing over time. In classical logic a statement can only be true since negative eternity and it will be true until eternity.
On the other hand, linear logic deals with statements like "I have a dollar" which can be spent on an ice cream. Therefore, at some point, "I have a dollar" was false, then it became true, and then it became false again.
It's also the logic that captures the difference between a reference and a value which is weirdly important. Unix's "everything is a file" should actually be recast as "everything is a reference".
The Rust borrow checker is based on a subset of linear logic and it's the secret sauce of said compiler. It can reason statically about dynamic systems.
I'll make some claims that I can support with papers if need to be so ask if you want proof. Currently, probability is based on measure theory however linear logic can also be used (Vovk bases probability on game theory which is essentially linear logic).
Generative adversarial networks (which are based on minimax) are based on linear logic as minimax is very linear logical.
I would go as far as to say that mathematics, in addition to axiom of choice also needs an axiom of adversarial choice. Axiom of choice assumes that you can always pick the best possible option, however you need to be able to account for your worst possible options as well. All mathematical optimization falls outside of classical logic.
The funniest thing is that this idea, the duality of things is very old. Dialectics is very firmly rooted in Western philosophy (Aristotle, Kant, Hegel, you know the usual suspects) however no one ever extended it to a formal logic.
They are essentially talking about linear logic, however the third rule is very much wrong, negation of negation is not a part of a logic of two opposites.
It can also be used as the foundation of probability instead of the more traditional measure theory.
The Muller’s Recurrence is a mathematical problem that will converge to 5 only with precise arithmetics. This has nothing to do with COBOL and nothing to do with floating and fixed point arithmetics as such. The more precision your arithmetics has, the closer you get to 5 before departing and eventually converging to 100. Python's fixed point package has 23 decimal points of precision by default, whereas normal 64bit floating point has about 16 decimal points. If you increase your precision, you can linger longer near 5, but eventually you will diverge and then converge to 100.
# Long version
What's going on here is that someone has tried to solve the roots of the polynomial
x^3 - 108 x^2 + 815 x - 1500,
which is equal to
(x - 3)(x - 5)(x - 100).
So the roots are 3, 5 and 100. We can derive a two-point iteration method by
x^3 = 108 x^2 - 815 x + 1500
x^2 = 108 x - 815 + 1500/z
x = 108 - (815 - 1500/z)/y
where y = x_{n-1} and z = x_{n-2}. But at this point, we don't know yet whether this method will converge, and if yes, to which roots.
This iteration method can be seen as a map F from R^2 to R^2:
F(y,z) = (108 - (815 - 1500/z)/y, y).
The roots of the polynomial are 3,5 and 100, so we know that this map F has fixed points (3,3), (5,5) and (100,100). Looking at the derivative of F (meaning the Jacobian matrix) we can see that the eigenvalues of the Jacobian at the fixed points are 100/3 and 5/3, 20 and 3/5, 1/20 and 3/100.
So (3,3) is a repulsive fixed point (both eigenvalues > 1), any small deviation from this fixed point will be amplified when the map F is applied iteratively. (100,100) is an attracting fixed point (both eigenvalues < 1). And (5,5) has one eigenvalue much larger than 1, and one slightly less than 1. So this fixed point is attracting only when approached from a specific direction.
Kahan [1, page 3] outlines a method to find sequences that converge to 5. We can choose beta and gamma freely in his method (Kahan has different values for the coefficients of the polynomial, though) and with lots of algebra (took me 2 pages with pen and paper) we can eliminate
the beta and gamma and get to the bottom of it. What it comes down to, is that for any 3 < z < 5, choose y = 8 - 15/z, and this pair z,y will start a sequence that converges to 5. But only if you have precise arithmetics with no rounding errors.
For the big picture, we have this map F, you can try to plot a 2D vector field of F or rather F(x,y) - (x,y) to see the steps. Almost any point in the space will start a trajectory that will converge to (100,100), except (3,3) and (5,5) are stable points themselves, and then there is this peculiar small segment of a curve from (3,3) to (5,5), if we start exactly on that curve and use exact arithmetics, we converge to (5,5).
Now that we understand the mathematics, we can conclude:
Any iteration with only finite precision will, at every step, accrue rounding errors and step by step end up further and further away from the mathematical curve, inevitably leading to finally converging to (100,100). Using higher precision arithmetics, we can initially get the semblance of closing in to (5,5), but eventually we will reach the limit of our precision, and further steps will take us away from (5,5) and then converge to (100,100).
The blog post is maybe a little misleading. This has nothing to do with COBOL and nothing to do with fixed point arithmetics. It just happens that by default Python's Decimal package has more precision (28 decimal places) than 64bit floating point (53 binary places, so around 16 decimals). Any iteration, any finite precision no matter how much, run it long enough and it will eventually diverge away from 5 and then converge to 100.
Specifically, if you were to choose floating point arithmetic that uses higher precision than the fixed point arithmetic, then the floating point would "outperform" the fixed point, in the sense of closing in nearer to 5 before going astray.
First of all, forget about the "situation in Germany". Work is everywhere, so be willing to accept work anywhere. There's definitely a pecking order in consulting firms and you can get projects because the company gets a one off engagement with a new client who wants the work done on site. The company has some really awesome full time employees who could do it in their sleep, but they're busy on long term contracts with key clients. Be willing to go, as a subcontractor, to some unglamorous location for a week long project to pentest some shitty internal application that nobody has ever heard of. Get a few of those under your belt and you'll know how it works.
Second, understand that there's more to it than your technical skills. Make friends who work in the industry. Talk with them about what they're working on. Find any interesting bugs or behavior in what you're working on? Chat with them about that. Doesn't really matter if it's security related or not. The people who do the work in the industry are all generally interested in the details of software. If you're into that, then you belong.
Keep reminding your friends that you're hungry for work. Keeping in touch will keep you in mind when they need an extra guy to help out.
Once you start getting work be sure you contribute well. Everyone wants to have the most high severity findings, and obviously you will need to produce those if you wanna keep getting work, but also be that guy who goes the extra mile to help put the report together, write up extra recommendations that would be helpful.
Keep in touch with the people you work with. Be cool to the sales/project management/accounting people. It's simple things like getting your expenses/timesheets/invoices filed in a timely manner. There's more to the business than finding vulnerabilities. Everyone wants to close out the job, get paid, and move on. Show everyone that you know how to behave like a professional. Remember that the people responsible for staffing are asking themselves: Who do we know that we can send in there to take care of this work, so that we can bill them and collect this revenue, who will get the job done and be easy to work with?
Be that guy, and you will be approached too, and you can find full time work in the industry if you want.
> A solution might have been to switch back and forth from Protected Mode. But entering Protected Mode on the 286 is a one way ticket: if you want to switch back to Real Mode you have to reset the CPU! Bill Gates, who understood very early all the implications, is said to have called the 286 a “brain dead chip” for that reason.
Even if you never wanted to go back to real mode, the 80286 was brain dead because of the way they laid out the bits in selectors. One small change to the layout would have prevented so much pain for programmers.
In protected mode, like in real mode, the 286 used a segmented addressing scheme.
In real mode, an address consists of two 16-bit parts:
The mapping to physical address uses a lookup table, indexed by the selector. The table entry, which is called a "descriptor", contains the physical address of the base of the segment. The offset is added to that base to get the physical address. The descriptor also contains information about the segment, such as its length and access permissions.
There are two lookup tables available to the program at any given instant. The T bit selects which is used. If T is 0, it uses a table called the Global Descriptor Table (GDT). If T is 1, it uses a table called the Local Descriptor Table (LDT).
The GDT, as the name suggests, is global. There is a single GDT shared by all code on the system. Typically it is used to map the segments containing the operating system code and data, and os protected so that user mode code cannot access it.
Each process has its own LDT.
The RL bits specify the Requested Privilege Level (RPL). The 286 has four privilege levels, 0-3, with lower numbers being higher privilege. To determine if access is allowed, the processor looks at RPL, the provilege level given for the segment in the descriptor (DPL), and the privilege level the processor is currently running at (CPL). The check is max(CPL, RPL) <= DPL. It's OK for user mode code to set RPL to whatever it wants, because it runs at CPL == 3, so RPL has no effect.
Let's look at this from the point of view of a user mode C program running on a protected mode operating system. The address space as seen by the C program, viewed as a 32-bit unsigned value, looks like this:
00040000 - 0004FFFF first 64k
000C0000 - 000CFFFF second 64k
00140000 - 0014FFFF third 64k
...
Note that if you are stepping through your address space, every 64k the address jumps by 0x70001 instead of the more usual 1. This makes pointer arithmetic take several more instructions than it would on a machine with a flat addresses space.
To prevent making all programs incur the performance hit from that, the compiler writers gave us several different memory models. If you compiled a program with "small model" [1], the compiler would limit it to a single 64k code segment and a single 64k data segments. It could load the CS and DS segment registers once at launch, and treat thee address space as a 16-bit flat space. In "large model" it would do multiple code and data segments, and incur the overhead of dealing with pointer arithmetic crossing segment boundaries. There were mixed models, that had multiple code segments but only one data segment, or vice versa.
The C compilers for 286 protected mode added new keywords, "near", "far", and "huge" that could modify pointer declarations. If you declared a point "near", it was just an offset within a segment. It had no selector. A "far" pointer had a selector and offset, but the selector would NOT be changed by pointer arithmetic--incrementing past the end of a segment wrapped to the beginning of the segment. A "huge" pointer had a selector and offset, and would include the selector in pointer arithmetic, so that you could increment through to the next segment.
Now throw in needing to link to libraries that might have been compiled using a different model from the model your code is compiled with, and that might be expecting different kinds (near, far, huge) pointers than you are using, and all in all it was a big freaking pain in the ass.
They could have avoided all that pain with a simple change. Instead of addresses in protected mode looking like this:
Then the address space would like like this, from the point of view of a user mode C program looking at addresses as 32-bit unsigned values:
80000000 - 9FFFFFFF 524288k flat address space
If they had done this and also flipped the meaning of the T bit, so 0 means LDT and 1 means GDT, we'd have the address space look like this:
00000000 - 1FFFFFFF 525288k flat address space
A C compiler might still have offered near, far, and huge pointers, but now that would just be an optimization programmers might turn to if they needed the last possible bit of speed or needed to squeeze their code into the smallest possible amount of memory, and were willing to go to the pain of arranging things so pointer arithmetic would never cross a 64k boundary in order to do so. 99% of programmers would be able to simply pick "flat" model and be done with it.
Why didn't they do this?
I've heard one theory. The descriptors in the GDT and LDT were 8 bytes long, so the physical address of the descriptor is 8 * selector + base_of_descriptor_table. Note that the selector in the segment register:
is already shifted over 3 (e.g., multiplied by 8), so the descriptor lookup can be done as (segment_register & 0xFFF8) + base_of_descriptor_table. The theory is that they put the selector where they did so they could do it that way instead of having to shift it.
My CPU designer friends tell me that this is unlikely. They tell me that when you have an input to some unit (e.g., the selector input to the MMU) that is always going to be shifted a fixed amount, you can build that in essentially for free.
and had gone with T == 0 for LDT, then a protected mode operating system could allocate up to 196592 bytes of consecutive physical memory, and set up consecutive descriptors to point into that memory offset from each other by 16 bytes, and the address space would then look like the first 196592 bytes of real mode address space. That might have allowed writing an emulator that could run many real mode binaries efficiently in protected mode.
[1] I might be mixing up the names of the various memory models.
> With unspecified behavior, the compiler implementer must make a conscious decision on what the behavior will be and document the behavior it will follow.
No, what you described is implementation-defined behavior.
It may be confusing, but here's the breakdown of different kinds of behavior in the C standard:
* Well-defined: there is a set of semantics that is defined by the C abstract machine that every implementation must (appear to) execute exactly. Example: the result of a[b].
* Implementation-defined: the compiler has a choice of what it may implement for semantics, and it must document the choice it makes. Example: the size (in bits and chars) of 'int', the signedness of 'char'.
* Unspecified: the compiler has a choice of what it may implement for semantics, but the compiler is not required to document the choice, nor is it required to make the same choice in all circumstances. Example: the order of evaluation of a + b.
* Undefined: the compiler is not required to maintain any observable semantics of a program that executes undefined behavior (key point: undefined behavior is a dynamic property related to an execution trace, not a static property of the source code). Example: dereferencing a null pointer.
Your browser is drugged and forcefully robbed, at this point - not asked nicely. Something like uBlock/Easyprivacy is your browser saying no and refusing, but now I see providers trying everything possible to identify you and try to bypass everything on this.
I've seen providers attempt to access your GPU info, fingerprint you via 3D rendering, all sorts of disgusting stuff. They attempt to enumerate megabytes worth of plugin names and mimetypes, load Flash, Shockwave, Java, Silverlight, Windows Media, anything to exfil as much data as they can about you.
They buy thousands or tens of thousands of random domains, subdomains, and attempt all of them if they fail. They act like malware.
They serve fake sourcemaps that try to track the fact that you attempted to investigate them, and use this against you.
I've seen ads _port scan you and your LAN via websocket_ after using RTCPeerConnection and enumerating your local IPs.
I can think of many companies that do this immediately on first page load, silently, before you get a chance to read their ToS or opt out. There is no opt out. They serve this code with CNAMEs and via reverse proxies for first-party cookie access and adblock bypassing.
I think one of the greatest things about the M68K today is that it's a relatively powerful processor that's relatively straightforward to program and it's pretty easy to design hardware that uses it.
A single board computer with the m68k is still small enough that you can comprehend the schematics and build it at home (e.g. http://www.kswichit.com/68k/68k.html ), and it's a very valuable learning experience.
> I think that it was something along the lines of some implementations (including TianoCore) required the ExitBootServices call to be performed more than once to exit the UEFI-controlled environment correctly?
As hinted at in andreiw's reply, this is entirely spec-compliant (if really annoying). Quoting from the spec:
"Firmware implementation may choose to do a partial shutdown of the boot services during the first call to ExitBootServices(). A UEFI OS loader should not make calls to any boot service function other than GetMemoryMap() after the first call to ExitBootServices()."
There's a few problems there, but these amount to UEFI being a terrible, abominable spec.
The specification doesn't say that an implementation must not change the memory map inside ExitBootServices, and in practice many runtime drivers clean up or even perform RT Data allocations in that path. This results in the "MapKey is incorrect" error returned to the caller. (I've seen some that modify ACPI and SMBIOS on the fly inside the ExitBootServices path, awful, awful, awful).
So yes, the program calling ExitBootServices must be written to retry the call even if it really did avoid sandwiching any calls to UEFI between the last GetMemoryMap and ExitBootServices.
The other big Achille's heel of UEFI in general is the SetVirtualAddressMap() RT call and RT Services support in general, but Tiano's driver model makes it particularly easy to shoot yourself in the face and end up with an implementation that forces the OS to call RT services with identity mappings or even with mappings for supposedly non-RT regions. Ugh. MMIO is a favorite one to "forget" to add to the memory map as an RT entry.
UEFI uses the PE format for binaries, but doesn't actually mandate how PE should be used or what the allowed relocations are. You could build a PE binary that amounted to, say, tons of executable segments, each of which will be a separate memory map entry. Now since UEFI doesn't mandate exactly how an OS will assign virtual addresses (for SetVirtualAddressMap), nor exposes relative grouping of memory descriptors (forcing the OS to relocate these keeping relative distances) I can imagine a situation where RT drivers could break if the OS decided to aggressively compact the address map or instead introduce random large VA gaps between RT memory map entries.
By the way: if you're interested in this, you might also be interested in the set of 9 (count them: 9) new cryptopals challenges we sold off to raise money for rural congressional races on Twitter:
It's not bad at all. You can always start with gcc -S to give you assembler output of a compilation, then modify as you want, or compare with the compiler.
As for an ISA, it's not clean but there's only so much you can do to an assembler language, so it's not that bad. And the docs are pretty good.
>but rather the other additional circumstances of the "solitary jail life" which are mitigated for "ordinary prisoners".
In my own comment, I wasn't clear enough that I also had this in mind. There's a lot you can do to make your own environment comfortable. In prison solitary, nothing at all.
- Handbook of Practical Logic and Automated Reasoning
- Software Abstractions
- The Little Prover
Yes, currently I have Athena, OCaml, Alloy, ACL2 (via Dr Racket/Dracula) all up and running to work through the exercises in these books. I'm very skeptical anything will come of this, but it interests me and I can see the value.
His post and yours both oversell the problems while underselling the successes. It’s best to keep big picture in mind. Yes, it’s extremely hard. Yes, we shouldn’t rely exclusively on it or have too much expectations. On Guttman’s end, the Orange Book of TCSEC (later, EAL7 of Common Criteria) required many activities like I included in my own security framework:
Each was supposed to check the others. Each time, you want experienced people doing it since it’s the people that make these processes work. What’s mostly missing in this post and esp in Guttman’s is all the evidence of defect reduction. Most of the work he cites were tracking problems they found throughout their lifecycle. They all said the formal specifications caught bugs due to ambiguity. Some found formal proofs beneficial with often mentioning “deep” errors they likely wouldn’t find with testing or code review. TLA+ use at Amazon was great example where errors showed up 30+ steps into protocols. Most of old verifications found they caught errors just simplifying their specs for the prover even if they wouldn’t run proofs. And for high-assurance security, the A1-class systems would go through 2-5 years of analysis and pentesting where evalutators said they did way better than systems using mainstream practices. Most of those can’t even tell you how many covert channels they have.
If you’re interested in methods that helped in practice, I dropped a start on a survey paper on Lobste.rs trying to shorten several decades worth of material into an outline post:
Now, all that said, full proof is hard with a lot of problems. You hit nail on the head about the infrastructure problem. I’ve always strongly encouraged people to concentrate on building up one or two projects to have infrastructure for most common ways of solving problems in programming with as much automation as possible. They have at least been building most things on Coq, Isabelle/HOL, HOL4, and ACL2. Having prior work to build on has been helping them. As you’ve seen, though, they’ve not made this a priority: the tooling still is horrible. So, horribly-difficult work with horribly-difficult tooling. That leads to the next proposal I did that might help you or some of your readers who want 80/20 rule of most benefits without most problems:
Here’s my recommendation in general. Learn lightweight methods such as Meyer’s Design-by-Contract for most stuff, TLA+ for concurrency/order, Alloy for structure, SPARK for low-level code, and so on. TLA+ on distributed stuff seems to sell people the most. With a formal method in hand, then apply this methodology: memory-safe language + lightweight method to model-check important stuff + Design-by-Contract + tooling to generate tests from specs/contracts + fuzzer running with runtime checks enabled. This combination will bring the most quality improvement for least effort. In parallel, we have the experts formally verifying key components such as kernels, filesystems, network stacks, type systems, compilers, security protocols, and so on. They do so modelling real-world usage with each one coming with contracts and guidance on exactly how they should be used. The baseline goes up dramatically with specific components getting nearly bullet-proof.
Also, you said you wanted entire system to be reliable. There was one that set the gold standard on that by noting how everything failed with systematic mitigations for it in prevention and/or recovery:
The OpenVMS clustering software alone let their systems run for years at a time. One ran 17 years at a rail yard or something supposedly. The NonStop systems took that to hardware itself with them just running and running and running. Applying a combination of balanced assurance like I describe, NonStop techniques for reliability, and Cambridge’s CHERI for security should make one hell of a system. You can baseline it all with medium-assurance using tools that already exist with formal verification applied to a piece of the design at a time. The work by Rockwell-Collins on their commercially-deployed AAMP7G’s shows that’s already reachable.
The question that needs to be answered is not, "But the guarantees that we expect are much stronger than a correct protocol, handshake, or compiler optimization. We need the entire system to be reliable, and we need proof effort to be minimal for widespread adoption to be feasible." (Pretend that's a question, ok?) The question that needs answering is, "what is the easiest way to provide (strong) guarantees that the code is reliable?"
If you wanted to write a filesystem, how much work would you have to put into it before you could consider it "reliable" using traditional techniques? If it is 10x more than it would take to simply write the code, then "MIT’s FSCQ file system, developed over about 1.5 years using Coq, the complete system was 10x more code than a similar unverified filesystem. Imagine that — 2000 lines of implementation become 20,000 lines of proof!" doesn't sound so bad, does it? And 10x is not necessarily a bad estimate---unit testing alone would account for 2x, at a rough guess, and not only does it not cover all possible executions, it also has a reputation in this neck of the woods of focusing on the happy path.
"An Empirical Study on the Correctness of Formally Verified Distributed Systems" has been discussed here before (https://news.ycombinator.com/item?id=14441364) but I'd like to mention one quote from it:
"Finding 9: No protocol bugs were found in verified systems, but 12 bugs were reported in the corresponding components of unverified systems. This result suggests that recent verification methods developed for distributed systems improve the reliability of components that, despite decades of study, are still not implemented correctly in real-world deployed systems. In fact, all unverified systems analyzed had protocol bugs in the one-year span of bug reports we analyzed."
(And speaking as a guy who has some network protocol experience, some of the bugs that were found in the "shim" layers were...likely caused by inexperience: no, TCP does not preserve write boundaries on the recv end, and yes, UDP will duplicate packets under some error conditions.)
I will admit that many of the author's specific complaints are completely true. This quote should be in big letters in the introduction to any formal verification work: "On top of all that, if any spec or implementation changes even slightly, all the specs, impls, and proofs that depend on it will change as well. This makes even small changes a huge pain." And Coq is something of a pain in the rump. (I encourage anyone with a few spare hours to work through Software Foundations (https://softwarefoundations.cis.upenn.edu/); it's a lot of fun but at the same time very frustrating. [That should be "many, many spare hours". --ed.]) The least damning thing you can say about Coq is that it's not very well engineered. On the other hand, SMT solvers like the kind of thing behind SPARK and Frama-C are brilliant when they succeed in finding proofs but when they fail,...well, they light up a "?" on the dashboard and expect the experienced driver to know what the problem is. Further, they're rather limited on the programming features you can use with them---Dafny and the Java verifiers have garbage-collected languages, alleviating some of the pain.
But still, to address the author's fundamental issue,
"I went into the class believing that formal verification is the future — the only solution to a world of software ridden with bugs and security issues. But after recent events and a semester of trying to apply formal methods, I’m a serious skeptic. In this post, I’ll discuss why I think formal verification has a long way to go — and why it just doesn’t work right now."
I'm probably the wrong person to discuss this question with. I don't know more than I've written above. All I know about this is from conversations with Christian Urban, who implemented Nominal Isabelle. It was a while back, maybe the problem of implementing nominal techniques in constructive type theory in an effective way (i.e. doesn't put additional burden on automation) has been solved by now.
The problem as I understand it is this.
Let's say you have a theory T in the formal language given by
signature S.
- In HOL you extend T to T' and S to S', but the deltas between T and
T', and S and S' are small, and largely generic. This is possible
because almost everything handling nominal can be done using double
negation.
- In CoC you extend T to T' and S to S', but the deltas between T and
T', and S and S' are huge, and largely non generic.
