Hacker News Reader

Formal methods and "proving" "correctness" have not taken off because while they seem like a great idea, it's insanely expensive to do it for non-trivial software, and you end up with a provably correct piece of software that is still full of business logic bugs and which inevitably fails to keep up with ever-changing business processes.

I agree that software is terrible, and programming language choice plays a big role in what sorts of mistakes you can make, but I'm skeptical that attempting to write provably correct programs is a remotely realistic goal. Sure, it's possible to prove an algorithm, but the real world software systems that need the help--certainly anything that involves more than one process on a single CPU--have complexity that goes well beyond what can be modeled or reasoned about, much less be proven.

It's not that hard to automatically prove that a large piece of software has no buffer overflows and no null pointer dereferences. We had that working decades ago.

Unless the code is in C. Then it's really hard.

Ada may vaguely resemble Lua but aerospace grade code (think SPARK) is about as fun to write as assembly. Rust is not perfect but it has momentum and tons of free tooling. At this point it would be easier to just try to add more safety features to Rust than push for the adoption of a language without the conveniences expected of a post-Y2K programming language.

Difficult, yes, but solved [1]. There exist sound static analyzers for C and C++. "Sound" meaning no false-negatives.

[1] https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/REA...

How does this deal with higher-order functions? This is usually where these analyzers fall down. If you don't allow higher-order functions, then you just forbade virtual methods, so your analyzer can't handle real-world C/C++ code.

Off-hand, I don't know how it handles higher-order functions. It analyzes LLVM IR, not the source directly, so I guess it depends on how virtual methods are represented in LLVM IR and whether those instructions are supported or ignored by the tool.

The tool doesn't claim to handle everything, and doesn't claim to be complete. You can absolutely write code that it can't analyze because it's either too complicated or you're using unsupported language features. If you want your code to be analyzable, then you have to write it that way. The tool isn't magic.

Don't you think it's an over-statement to say that it can't handle real-world code if it doesn't support higher-order functions? Not all C++ code uses virtual methods, and C doesn't even have this feature in the language.

It's really not that hard, but it's important to remember that while these tools do guarantee no undefined behavior, they may require either adding annotations or changing the program a bit. Their goal is to guarantee lack of UB not for free, but at a cost that's drastically lower than a rewrite in a safe language, something they deliver on quite well.

So, for example, suppose you have a higher order function that takes a function returning a pointer, calls it, and dereferences its return value. For simplicity, let's assume we only care about NULL dereferencing and not other kinds of invalid memory, but the idea is the same. You then have two options: either you annotate the argument to require that it cannot return NULL -- in which case the tool would attempt to prove that any function passed as an argument satisfies this (possibly with the help of further annotations) -- or you add a runtime check, in which case the automatic proof is simple.

No false negative sounds nice, but the problem is the amount of false positives. The Unix `true` command is also a static analyser with no false negative (but 100% false positive on perfect code).

And a perfect static analyser with no false negative or false positive is equivalent to solving the halting problem. So what we need is a «good enough» solution working with existing code. But the amount of CVEs and the low adoption of such tools empirically shows that we are far from there.

This particular tool lets you trade analysis time for accuracy (amount of false positives) depending on your choice of settings, which is pretty neat.

If this has solved the issue of automatically proving that any C or C++ program has no buffer overflows, why do we still see CVEs for popular libraries and software that result from them?

Neither FOSS projects nor commercial software use proven methods most of the time. That's why you see the results you see. I described that here:

http://www.ganssle.com/tem/tem372.html#article4

The tools can also miss things. They miss more as complexity goes up. High-assurance systems used to structure things in a hierarchical way with simple functions and only call downs to aid the analysis. Basically, reduce combinatorial explosion. Most software isn't structured anything like that. It does combinatorial explosion with C not giving analyzer a lot of information to begin with. So, it causes tools to miss things.

Rust might be easier to analyze due to the type system. Those labels become inputs and heuristics for future static analyzers.

`Sound' does not mean `complete'. Don't forget that no false positive or negative isn't all, the solver might just give up.

Because people can't resist chasing proven incorrect code ("find bugs"), instead of overhauling programs for proven correct code. Because the latter is a lot of work.

There's a engineering-oriented middle ground that doesn't prove everything mathematically from first principles like Coq. Languages like Ada and Haskell can get you a long way without formal proofs.

It's hard because most languages do not help with that. There's not an easy option to get all the potential unhandled error sites for a code base. Even in Rust you can sprinkle your code full of "?" and you transformed back into runtime errors. Which is okay, if you understand it. It'd be great if such programming decisions could be annotated, then when someone imports a library it'd be easy to get a human readable list of potential runtime errors (edge cases).

But usually when it's time to just churn out yet another app, cost-benefit analysis indicates that fuck that, let's use pokemon error handling.

And it's hard to blame anyone for such a decision when the alternative is going a few more days without the shiny new app/feature. The end of the financial quarter is coming. The app/feature must "work".

And that's why it's not surprising that no one uses Coq and Idris for run of the mill business as usual apps.

? doesn't transform anything back into a runtime error. It's explicitly saying "I don't know how to handle any errors that happen here, so give it back to the caller." The "potential unhandled errors" are all still perfectly listed inside the return type.

Uh, thanks! You are completely right. I forgot that it's not just an unconditional unwrap.

What I wanted to communicate is that I find that in many cases error handling is a sort of twilight zone. When the environment or context of the running program is not what it should be. (Eg file not found, lack of permission to write to it, not enough memory, something is not configured, missing runtime dependency; and all the state validation errors, etc.) And the errors that result from this are usually too low level, and there is rarely enough information in the error messages (types) themselves to help understand (and potentially work around) the condition causing the error.

I'd say it's a fundamentally hard problem, instead. See halting problem.

Proving correctness is always an incremental win when executed correctly. Everything that can be proved correct is one more bug that your editor will underline in red, and often one less test to be written.

Agreed. Ada 2012 [1] and Spark [2] (an Ada subset with formal verification features) provide production-ready versions of most of these features.

Clojure's spec [3] is also promising for better specifications and more automated testing

Over the past decade or so, we have seen many mainstream programming languages adopt functional programming features. My hope is that more mainstream languages adopt preconditions, postconditions, invariants, and useful formal verification features. There are so many more great tools that could be used to build high quality software than unit testing.

[1] https://www.ada2012.org/

[2] https://en.wikipedia.org/wiki/SPARK_(programming_language)

[3] https://clojure.org/about/spec

If you look at the issue linked in the Rust tracker from the article, the people discussing this are specifically referencing Ada and SPARK.

https://github.com/rust-lang-nursery/wg-verification/issues/...

Nice! I did not have a chance to look at the issue discussion. Thank you for pointing it out.

It's good to see that Rust is learning from Ada. Ada is also learning from Rust: https://arxiv.org/abs/1710.07047

C++20's getting contracts: https://en.cppreference.com/w/cpp/language/attributes/contra...

The Coders At Work interview with Fran Allen really hammered home that point. Which begs the question, why did C get so popular? I guess what programmers like to use isn't really what is always best for them. People like to ride motorcycles and programmers like to use C.

Some people would say that C got popular (apart from the obvious UNIX sponsorship) because at its core it is just a fancy way to address memory like in assembly, but almost portable.

Not exactly the same, using C is like driving motorcycles without helmet and protective gear.

These people are also known as "organ donors".

> Memory safety by proof was coming along well in the early 1980s. Working systems existed. Automatic prover technology was working. Then came C.

K&R was published in 1978. So at best this story and timeline are incomplete.

More illuminating would be an account of why C beat these other languages in the marketplace in the 80s, despite its disadvantages in safety.

Easy, it came with an OS, given away for a symbolic price, with source code tapes alongside.

Had Bell Labs been allowed to sell UNIX at the same price as other companies were selling theirs, and C would never have taken off.

Burroughs, developed in 1961 in a memory safe systems programming language is still sold by Unisys as ClearPath MCP.

Same applies to the IBM mainframes.

The surviving systems from the 60-70's where C only plays a guest role at most.

There is nothing wrong with the timeline. K&R may have been published in '78 but it really took over the industry by the '80s.

Because, C is portable assembler. In Pascal, for example, if something cannot be done in Pascal, then assembler must be used. If assembler is used, then program is tied to single platform. If you need to support two or more platforms at same time over long period, then C wins.

That is the myth, in practice ISO C specifies an abstract machine and libc is impossible to be written 100% in ISO C, some functions require either external Assembly or language extensions for their implementation.

Too many years are passed, but as far as I remember, only C code was portable between 8, 16, and 32 bit platforms. It was possible to incrementally convert program from assembler to C and then port to different platforms, but it was not possible to do conversion using Pascal, or other programming language.

Yeah, if you were writing using a safe subset across all C variants that happened to be supported across all those C compilers.

Check language support across Small-C, Turbo C, Quick C, Aztech C, Metrowerks C and many others from those days.

Likewise it was possible to do the same across Pascal compilers that implemented variants of ISO Extended Pascal/UCSD Pascal, Modula-2 and a couple of other high level languages.

I would also be curious what are all those things that C can do but e.g. Modula-2 cannot, when it comes to being a "portable assembler".

Naturally Modula-2 also faces the same issue. What it offers is better type safety and being honest about it.

The whole point is that contrary to its sales prospect, not only does C also require to write Assembly, it doesn't have any language support for modern hardware CPU/GPUs, just like any other high level language, requiring extensions to the standard, not necessarly portable across implementations.

C the language can be portable even if the libc is entirely in assembly. Of course you assume to have compiler/std on the platform you want to use it.

That capability is shared among all high level programming languages, nothing special about C here, once upon a time it was also only available to UNIX users.

My understanding is that C/UNIX were together portable between platforms. Portability of C between OS was relevant mostly later.

> Subscript checking optimizations had been figured out by the 1980s, so the performance penalty was coming down.

well, we're in 2019 and replacing a few critical .at() by [] regularly allows me to gain a few % when benchmarking.

That's because the C++ compiler has no idea what you're doing. It can't hoist subscript checks out of loops, because it doesn't know they're subscript checks. They're something some template generated, and at bottom, they expand to an IF statement. The Go compiler, which knows about subscript checks, does some of those optimizations.

For this optimization to work, the compiler has to be allowed to report subscript errors early. Frequent subscript checks that cause noticeable overhead tend to be inside loops. Often, the compiler could hoist the implicit assert inside the loop up to one assert checked before the loop is entered. It has to be allowed to report failure as soon as it become inevitable. If you have a loop from 0 to 100 over an array that's 0 to 99, and there's no way to exit the loop early, then failure is inevitable.

As soon as failure is inevitable, it has to be OK to detect it. That means if you're printing values 0 to 100, you'll never even get the first one printed. You'll abort before entering the loop. This is a bit strange to C/C++ programmers.

Once the assert has been hoisted out of the loop, the compiler may be able to prove that it can't fail. For FOR statements, this is usually easy. So the subscript checking overhead can completely disappear for many inner loops.

Then again, who uses at() inside a loop in C++? That's what iterators are for.

Plenty of enteprise developers that learned some kind of C++ long back when, and never bothered to improve themselves in this area.

I have seen plenty of code like that, specially when written by the occasional C++ coder that usually works in other languages.

doing math code which requires computations on indices with iterators is the best way to drive developers to suicide

> As soon as failure is inevitable, it has to be OK to detect it. That means if you're printing values 0 to 100, you'll never even get the first one printed. You'll abort before entering the loop. This is a bit strange to C/C++ programmers.

It's strange but compilers are allowed to do it and anyone sufficiently familiar with undefined behavior will not be surprised.

Compilers are not currently allowed to do it if “failure” is in the form of an abort from an inlined function, as in the case of .at(),

Ah, so the compiler doesn't understand it's a failure, and just sees normal program flow that it can't alter.

That's a tricky thing to solve, yeah. At best, under current semantics, the compiler could emit a fast loop and a slow loop, and pick which one using an initial bounds check. But that's extremely awkward at best...

Automatically handling the bounds check upfront is a type of control flow that's halfway between normal exceptions and undefined behavior, that C++ doesn't really grok.

When I dabbled in gfortran, a feature I liked was that while no bounds-checking is the default, run time bounds-checks can be enabled with "-fcheck=bounds" or "-fcheck=all", which can be handy while developing/testing code.

Alternatively, Julia has a macro "@inbounds" which disables checks, but this involves going through and annotating code after testing. You can also start Julia with the options "--check-bounds={yes|no}" to override declarations. Running testsuites enables all checks.

Seems like it would be handy if these checks could be elided by defining a macro. Any reason this isn't done?

The performance cost is often much higher than the time spent repeatedly checking bounds. It tends to defeat the auto-vectorizer.

Another workaround is to manually check bounds before the loop. This lets the compiler prove all bounds checks pass if it gets to the loop, and solves the problem. I do wish that sort of thing could be automatic.

If that's the semantics you want, why not just add a check at the beginning of the loop? Compilers could add a warning advising the developer to do this if she doesn't care about partial results, anytime that they can't fully eliminate an .at() bounds check inside a loop.

It's a matter of economics, mostly: proving that a feature is mathematically correct costs a lot more than implementing the feature itself, and so mathematic proofs are not done except if the cost justifies it.

And because of that the tools that do these proofs do not take off, and thus they get reinvented every few years with each programming language.