More on error management in Midori


#1

A very interesting article about Midori (I used to pay for articles far worse than this one):

http://joeduffyblog.com/2016/02/07/the-error-model/

I agree with most things written in this article.

There are two discussion threads on it:

Some notes:


void Foo() {
    Debug.Assert(something); // Debug-only assert.
    Release.Assert(something); // Always-checked assert.
}

Having such two kinds of assertions seems nice.


Transforming code that uses Result into code that uses exceptions automatically: seems an interesting Summer of Code experiment to do :slight_smile:


Contracts: I use them often in D, they are sometimes nice to have (pre-conditions, post-conditions, invariants, loop invariants, loop variants), and perhaps I’d like them in Rust too. They are also easy to understand and use, if well designed.

All contracts and assertions were proven side-effect free thanks to our language’s understanding of immutability and side-effects.

This is nice.

Contracts have recently became popular as an expression of program logics used in advanced proof techniques. Such tools prove truths or falsities about stated contracts, often using global analysis. We took a simpler approach. By default, contracts are checked at runtime. If a compiler could prove truth or falsehood at compile-time, it was free to elide runtime checks or issue a compile-time error, respectively.

But making the compiler catch some mistakes at compile-time makes ContractBasedProgramming more useful, especially for certain kinds of code.

But in D language we have seen that it’s a good idea to not let the compiler judge what to run at compile time. It’s better and safer to ask explicitly what you want to run at compile time. I have proposed to introduce “enum contracts” that are run at compile-time only (Ada language has similar things).

Modern compilers have constraint-based analyses that do a good job at this, like the range analysis I mentioned in my last post.

Adding some range analysis to Rust will be a big win!

Furthermore, the contracts a method declared were part of its signature. This meant they would automatically show up in documentation, IDE tooltips, and more. A contract was as important as a method’s return and argument types. Finally – and this was the nail in the coffin for me – contracts were supposed to be part of an API’s signature. What does it even mean to have a conditional contract? How is a tool supposed to reason about it? Generate different documentation for debug builds than release builds? Moreover, as soon as you do this, you lose a critical guarantee, which is that code doesn’t run if its preconditions aren’t met. As a result, we nuked the entire conditional compilation scheme. We ended up with a single kind of contract: one that was part of an API’s signature and checked all the time.

This is one of the very few points I don’t fully agree with… In D language you have a compiler switch to disable contracts checking. Most contracts are fast, but sometimes in a pre/post-condition you put an alternative simpler algorithm, that does the same as the main function, and you compare the two results. Such small algorithm is slow, so you don’t want to run such heavy tests all the time (but other solutions exist, like wrapping this heavy code in a “static if debug) {}”).


Range Types: well implemented range types (as in Ada, or better) and enumerated subsets will be really useful in Rust, avoiding bugs, making APIs more self-descriptive, and removing the need for lot of contracts and asserts. This is one of the few things I miss in D/Rust from Ada. Probably they need to be built-in, unless the compiler has very good handling of enum preconditions.


#2

Note: Because this statement will make absolutely no sense to anyone not familiar with D: a while back, D repurposed enum { ... } (Note: no identifier) for ephemeral constants. The Rust translation in this context would be to const.


#3

Right, sorry. (I will probably have to give some examples both in what Ada2012 does, and what I proposed for D).