Hacker News Reader

Comment by catnaroek | Hacker News Reader

I'm not talking about changing languages, but rather about giving existing languages more rigorous specifications. My beef with C, C++, unsafe Rust, etc. isn't the presence of undefined behavior in arbitrary programs (for which the solution is very simple: don't write arbitrary programs!), but rather the absence of a calculational method [0] for designing programs that don't have undefined behavior (for which a formal semantics is an indispensable prerequisite). To convince yourself that a C program doesn't have undefined behavior, you need to interpret the English text of the C standard, and that's what I object to.

[0] The calculations needn't be performed by a machine. If they are performed by a machine, you have a safe language. If they must be performed by humans, you have an unsafe language, which is nevertheless a lot more usable than C and friends.

View on HN

fwiw this appears to be a goal of people working on speccing out Unsafe Rust stuff. You also don't need to worry about interpreting any english specs today, because there just aren't any specs at all yet!

I'd have to interpret the Rustonomicon, which is still written in English. :-p

There are some tools aimed roughly in this direction, such as https://github.com/TrustInSoft/tis-interpreter.

A major difficulty here is that undefined behaviour is a property of a particular execution of a C program, rather than a static property of the program itself. Tools that dynamically detect UB are useful, but will not demonstrate that there are no inputs for which a program will go wrong.

As powerful as an interpreter might be for running programs, it isn't the right tool for designing programs. Validating a program design requires static analysis, to be performed either mechanically (e.g., type checking) or manually (e.g., manipulating predicate transformers in the way advocated by Dijkstra).

If you take JS and add Flow, or Python and add MyPy, and then accept the judgment of the checker and don't use the parts it doesn't check, then it becomes a language subset -- and sort of a different language. Like if you have array bounds annotations and check all indexing operations, C arrays become Pascal arrays.

That's the thing - I'm not talking about using any mechanical checkers. I'm talking about using a language definition that makes it easier for humans to prove things about their programs.

Okay, that's interesting. How would that work in practice? It doesn't seem like it would be easy to apply in a timely way. If the rules can be unambiguously checked by humans, would they not be more efficiently checked by machines?

Proving theorems isn't just performing routine checks. There are creative aspects, like finding the right loop invariants, at which machines fare absolutely miserably.

OTOH, machines excel at exhaustive enumeration and enforcing separation of concerns: that's why ML-style algebraic data types, pattern matching and parametric polymorphism are such a boon for high-level programming.

So there's room for both human and machine work in program verification. What we should be interested in is finding the right division of labor between humans and machines.

One can use clang and gcc to either produce a runtime error if undefined behaviour is detected or that and abort the program.

There are several things, like signed overflow of integrals, that cannot often be determined at compile time.

I think the OP is referring to full-blown verification systems, like some dependently typed languages have (although they aren't the only ones). If your program's behavior is defined because you wrote it that way (i.e. not by chance), you would have an argument for why the undefined behavior is not invoked that could be translated into a formal proof in most sophisticated (i.e. ZFC-ish) formal systems.

Formal verification, yes. Mechanical verification (dependent types, SAT/SMT solvers, model checkers, etc.), not necessarily. I don't mean to insult the efforts of the mechanical verification community, but it's preposterous to suggest that the only way to verify programs is to use a computer. Hey, we have brains! We can use them too!

To my knowledge the undefined behavior sanitizers are not complete. It is also unclear how you both optimize your program (exploiting undefined behavior semantics) and providing a runtime check without completely killing performance.

Use it during your unit tests, clang claims the runtime cost is small so it might now matter either.

As useful as debugging tools are, they are no replacement for design tools.

Reply on news.ycombinator.com