re. arXiv, my point was that you could have submitted the URL https://arxiv.org/abs/1602.07455 instead of https://arxiv.org/pdf/1602.07455, and that I think in general it’s good hygiene for articles in an open-access archive. (I agree with your preference on citing authors and publication year when you cite a work, and I apply them in in-text citations, although I understand that lobster has a policy on titles that suggests only including the title. If you link to the arxiv web abstract instead of the pdf documentations, the terse title is never an issue as the metadata is all available on the landing page.)

“We are in research pase” is a bad reason not to show code. It’s a bad reason before you get a paper out, but it’s an even worse reason once you had your publication confirmed (and indeed the authors mention that they got an ICDE18 paper out of this work). Research is about sharing ideas in the open, and talking proudly about your work on a specific software prototype without giving the sources is a douche move.

these folks have a decent pedigree both with respect to research and open sourcing their code. I haven’t looked closely at the paper yet, but the numbers seem non crazy. that said, as with all the work in this particular sub area, consistency models mean everything, and the words “flexibly consistent” a guaranteed to be doing a lot of work.

“you seem to disagree with formalism and believe only in experiments”

The amusing thing is that his experiments use formal methods in form of numbers, algebra, probability, and propositional logic (i.e. computer gates they run on), possibly model-checking (i.e. concurrent algorithms they use). He seems to trust math given he derives empirical results by plugging data into such mathematical formulas. That’s what people do with formal verification. Except, there’s both more a faith-it-works aspect and higher error margins with the statistical math versus the simpler forms of logic used in program verification. Maybe there’s something I’m missing but empirical methods seem highly dependent on math functions and reasoning on output of math functions. For some, especially probabilistic vs simple logics, it also looks to take more trust to believe statistical models than logical ones.

I’ve been thinking on that since he first started talking about superiority of [math-based] methods he called emprical being better than math-based methods others called formal. I dug up some articles today in what spare time I had to further explore this contradiction. I was guessing core areas of math/logic could probably be considered empirically proven given all field data confirming the basic primitives and rules in them. The stuff I was finding was corroborating that or vainly trying to reject falsifiability due to math’s abstraction level. I might post some references or summaries in the future on this topic when I have more time and sleep.

Your accusation of this work being a “cargo cult argument” is highly unfair. The authors built an implementation of a GMP-like library and defined a specification for it, such that a computer can verify that the implementation matches the specification. This is a very strong argument in favor of the correctness of their implementation, not cargo-culting.

This sort of work is possible to do in C (see Frama-C, VeriFast) but fairly difficult, due to the complexity of the full semantics of the C programming language. Instead, the authors work in a language designed for formal verification, whose semantics is easier to reason about – and with good tooling support for automating verification – writing their program in such a style that they can translate it back to C.

For a given specification of what a piece of software should do, it is reasonable to assume that a program that has not been verified against this specificatin has a higher likelihood of having defects than a program that was verified against the specification. There is nothing cargo-culted in that.

There’s been bugs reported in GMP already. Range errors are also common vulnerabilities in general case. How much stronger case needs to be made at that point that immune by default is better position?

If a C code base includes calls to unsafe functions like strcpy(43), sprintf(29), strncpy(27), or strncat(1) then it seems likely that one or more of them incorrectly computes the length of a string.

Certainly, but still I am a bit confused by this blog post that seems to imply that this function is not typable with traditional HM algorithms for prenex polymorphism, while it does seem to work just fine. Is there an error in the blog post itself, and the author meant to insert an example making essential use of higher-order polymorphism? Or was there a bug in the previous type-checker that could have been fixed while keeping the same inference specification, instead of moving to higher-rank bidirectional algorithms?

I believe that these tools are not based on parametricity, merely on syntactic proof search (in essence, enumerating possible terms at this type, using techniques from the proof search literature). If you think about it, theorems-for-free does not actually help you generate code at arbitrary types.

I don’t believe in “labor pool” as an explanation of the difference. FOSS communities do not have a formal methods culture, at all. When academia shows up with ideas of tools to adopt to improve software production, they are met with a lot of implicit resistance and “I won’t do anything until the tool is super easy and convenient to use”.

In contrast, Microsoft has managed to introduce formal-methods tools in its development process; I suspect by a lot of top-down authority moves “here is how we’re going to do things now”, but I don’t actually know how the changes happened internally. I’m sure it had costs, because the tools were not necessarily able to scale to the project’s scale on day one, and there certainly was a lot more necessary work poured into making them easier to use after they started getting adoption internally.

Personally I think that the lack of interest for formal methods and, in general, most sorts of interaction with academia that do not fit the existing “just send us patches in the way we are used to” workflow (those do happen, for example the systems research community contributes to Linux, and the compiler people contribute to GCC and LLVM), is one of the main issues with open-source communities today.

The Linux kernel, for example has a lot of companies funding its development today, it’s not a volunteer-on-their-spare-time project, yet almost no one is willing to get serious about interacting with academia (somes exceptions I know of are Coccinelle, and the recent work on formalizing Linux memory models and in particular the RCU mechanism, which happened in great part thanks to the motivation of Paul McKenney).

It is not a “open-source vs. industry” split, because a large part of industry is just as bad at interacting with academia. Actually Microsoft is in a rather unique position there, given the long-term investment they made in Microsoft Research, so it’s understandable that they would be better at else than pretty much everyone else. (IBM still does have some good research groups, and I’m sure Intel has interesting stuff in hardware-land and physics but not that much in software as far as I know.)

“Projects that are primarily driven by volunteers working for free on their limited free time tend to have a labor disadvantage, especially for any subproject that would require cooperation and long term sustained, focused effort from multiple individuals.”

Ok. I misspoke in prior post. Let me modify it to say they have potentially a labor advantage where the contributors are free and not forced to use whatever tools companies demand. You’re right in that the actual affect is usually either no contribution or low amount that’s hit and miss. The big ones are outliers.

“Finding all the things that break and fixing them can take a lot of time, but they can all be handled as individual incidents in isolation, and then you move on.”

This is an interesting perspective. It could be a psychological motivator for some of these activities. I know two others that we must remember, though. One is backward compatibility with UNIX model. That architecture dictates quite a bit in terms of what they can do with what results. The other is they prefer mitigations that have barely any observable slowdown that also work with little effort by users. The usability aspect is great default but the other thing means they’ll use risky mitigations or obfuscations. Those addressing the root causes almost always have a significant slow-down if still using C language. So, UNIX model, on by default, little to no performance hit, and maybe like you said easy to work on a little at a time.

Your point would probably apply to other projects even more since the OpenBSD team is unusually committed to doing the hard work.

“Introducing the straight jacket of verification and provably safe code (but who proves that the proof proves the right thing?) is much more like revolution. We all know you just don’t slap C with it, fix a few dozen bugs, and be done with it.”

You actually can if aiming at medium assurance. As I told one of them, the least-painful option would be to create a safe variant like Cyclone that integrates well with C in terms of calling it or compiling to it.

https://en.wikipedia.org/wiki/Cyclone_programming_language

New code can be written in Cyclone or similar language. Old code can be gradually rewritten over time or they can do a big rewrite. The language differences amount to annotations or differences in structuring where you usually don’t have to change the actual algorithms. The port wouldn’t be easy since they never are. It would be way easier than a non-C language and easier than trying to make everyone experts at never introducing vulnerabilities in C code. Integration with tools such as Frama-C, KLEE, affine types, or assertion-based test generation would just make the quality go through the roof if supplementing their code review.

That’s all before we even consider things like formal verification done by hand or really changing the structure of the OS. The safe language option is quite doable. Especially seeing what Redox OS did in Rust and Muen kernel + IRONSIDES DNS did with SPARK Ada. Those projects would be harder given the borrow checker or annotations than C developers using a safer C or something w/ lightweight, verification tools. What stops them is personal preference of the team far as I can tell. They just like using C, want a UNIX, prefer to do the code review, and so on.

“who proves that the proof proves the right thing?”

That’s barely relevant even though I see why you’d ask. Your TCB always includes your requirements, design, source, tooling, underlying platform, and so on. All you can do is reduce it and make it easier to verify. Decades of evidence shows formal specifications in particular find problems in many parts of the lifecycle, esp ambiguities or interface errors. Formal proofs can find nearly impossible-to-spot bugs but seem to be best for tiny, critical stuff that’s similar to prior, verified work so you know it’s possible to do in the first place.

Far as how deep trust goes, a lot of this work is done in Coq or HOL specifications. HOL itself has been verified at a logic level with another person making a low-TCB implementation, HOL/Light, being a few hundred lines of code IIRC. Foundational, proof-carrying code and other methods essentially use a prover to generate all the transformations from high-level specs or source down to assembly producing proof terms in as untrusted way as possible. The trusted, lightweight checker such as HOL/Light then confirms each action was logically valid in the rules of the logic and in terms of the formal specification. You essentially trust a pile of unambiguous specifications which are easier to machine-check plus a checker that’s easy to check. Examples from a leading researcher:

https://www.cl.cam.ac.uk/~mom22/stacks.html

So, there that is for your curiosity. They’ve taken it much farther than I ever expected reading about the old days of Gypsy Verification Environment, VDM, and so on. With work like CertiKOS, the field has come a long way. :) That kind of thing takes a lot of PhD’s. So, I don’t ask FOSS projects to do that much. Most I’d push is Cleanroom w/ safe languages or Altran/Praxis’ Correct by Construction. The latter combines good design, formal specs, code what one can in SPARK or something similar, thorough review of specs/code, and plenty of testing. Their defect rate is usually around 0.04-0.05 per thousand lines of code with some provably immune to common vulnerabilities. It seems practical given they charge a 50% premium on top of going rate for software projects by experienced professionals. As you said, though, raising the bar on quality using such specialist techniques will reduce contributions a lot. It can probably be done in a quality-focused project such as OpenBSD, though, since they already raised the bar quite high.

Does that mean that there is a space for an OSM mirror that would offer an API to others, having them pay for resource usage?

It’s my understanding that Apple does use OSM as a provider and contributes back.

On top of that, they (esp Ocaml) come with libraries specifically for writing compilers faster.

After using ASDL a lot, I definitely wondered if I should have written it in OCaml. In 2013, I did another parsing project in Python, and I actually resolved to write future projects like that in OCaml.

But there are a couple problems with OCaml. I would say it’s a meta-language for semantics and not syntax. ANTLR/yacc are meta-languages for syntax. In particular:

• OCaml’s Yacc is NOT good enough for bash. It misses by a mile. If you look at the first half of my blog, you will see I spent a lot of time developing a somewhat novel parsing algorithm for bash.
• Moreover, the VERY first thing you hit when writing a language – the lexer, is heavily stateful. OCaml is worse than C for writing this kind of code. Parsers and lexers are slightly paradoxical, because from the outside they’re purely functional, but from the inside they’re heavily stateful. I don’t like writing imperative code in OCaml; there’s no real benefit.

The second problem is that OCaml is not a good meta-language for itself. I talked about that in “Type Checking vs. Metaprogramming” [1].

So yes I’m daydreaming about a meta-language that’s a cross between ML/Lisp/Yacc/ANTLR – some details here [2]. But it is toward a somewhat practical end. I actually have to implement multiple languages (OSH, Oil, awk/make). If it can implement those languages, I’ll call it done.

Now, I’m not necessarily saying that OCaml would be worse than Python. I certainly worked around a lot of Python’s quirks, no doubt. But they both have flaws for this application, and I chose the one I was more familiar with and which had a bigger toolset.

[1] http://www.oilshell.org/blog/2016/12/05.html

[2] https://www.reddit.com/r/ProgrammingLanguages/comments/62shf7/domain_specific_languages_for_building_compilers/

The new one is bigger because it will have the functionality of Awk and Make.

Huh, this sounds a lot like mash: http://www.vitanuova.com/inferno/man/1/mash.html , http://www.vitanuova.com/inferno/man/1/mash-make.html

(aren’t “explicit effects” and “purity” in essence the same thing?)

I’d like to believe so but some people believe Haskell isn’t pure because we have partial functions :)

‘Sides, you could have explicit effects in something like Rust and still not be purely functional because it’s an imperative programming language. Adding explicit effects to OCaml would be much of the same. Y'all hacked some limbs off a dead cow and tacked them onto your lambda calculus, so purity’s a dead letter.

consensus on how to best achieve it, both in the theory and in the practice, is not yet clear

Monads work great for me and I have a range of methods at my disposal for working with them. mtl-style (nota bene: not the actual mtl library) has been best-of-all-worlds. I have not been impressed with Eff even when an entire language was catering to it.

You point out that Rust has traits, but that’s a strange narrative. Scala had implicits for a while

I point out Rust because it disallows orphans entirely.

Scala had implicits for a while

Not canonical, so not typeclasses. Implicits are terrible and not equivalent to typeclasses at all. This isn’t some hypothetical, implicit scope behavior in Scala bites users of Scala all the time.

Adding an import shouldn’t silently change the behavior of my code at runtime with no warning. That is obscene.

important consequence of demonstrating that coherence is not an issue in a dependent language

shrugs I’ve only kicked around tutorials in Agda, Idris, and Coq, whereas I work in and write about Haskell. I’d prefer to have the explicit option of making the overloading unique per type across the entire class for the sake of the humans reading and reasoning about the code.