Error Handling in Mechanical.md

(WIP) Error Handling in Mechanical

Appendix: Survey of Error Handling in Other Languages

• checked exceptions: Java

  • the most infamous is Java's widely hated checked exceptions. No one else does this afaik
  • good:
    • you can code the "happy path" in a "direct style", and handle abnormal situations separately
    • function signatures tell you exactly what exceptions can happen (except for the carve-out, see below)
    • checked exceptions make it a little harder to forget to use try/finally
    • try-with-resources statement copies Python's lauded with-statement
  • bad:
    • everyone hates adding throws WhateverException, AnotherException, YetAnotherException, OhYouForgotThisOtherException to all their methods
    • it's not really clear when you should subclass unchecked RuntimeException instead
    • try/finally is notoriously hard to use right, although this is largely addressed by try-with-resources

• unchecked exceptions: C#, subset of Java, Python, Ruby

  • C# hews most closely to Java, even using the same throw/try/catch/finally syntax, but exceptions are unchecked so there's no throws
  • Java itself has a pretty big carve-out where you can define your exception as a subclass of RuntimeException, all descendents of which are unchecked, and I'm pretty sure there are Java communities that make a point of systematically doing so
  • the practical result of unchecked exceptions in static languages like C# and Java is a pretty similar error handling story to dynamic languages like Python and Ruby
    • (they went with different syntax though: Python uses raise/try/except/finally, and Ruby uses raise/begin/rescue/ensure)
  • good:
    • you can still code the "happy path" in "direct style"
    • I believe Python pioneered the lauded with statement which largely addresses the try/finally footguns, and C# copied it as the using statement and Java copied it as try-with-resources (and a similar pattern is common in Ruby, not sure who got the idea from who)
  • cons:
    • unhandled exceptions are a pervasive form of runtime errors
      • because exceptions are unchecked, it's not super easy to figure out which exceptions you should catch and handle, or to remember that you ought to try to figure that out at all
      • it's very easy for the programmer to code the happy path, use try-with-resources correctly, but then not worry about handling any of the possible exceptions at all until they show up in production (or ideally, testing)

• just return error values, no specific language support: C, C++ (kind of? I think?), JavaScript, Clojure

  of course, C is particularly primitive, and C++ is particularly complicated

  • the convention in C is a particularly primitive version of this: return error codes which are actually int constants; the result of the operation is written to an out parameter; violations of an assumption may result in undefined behavior or if you're lucky, a crash
  • I don't really know C++ (does anyone?), I think C++ has an especially sprawling and varied community, but Boost, for example, recommends throwing exceptions to unwind the stack and induce destructors to handle cleanup, and not catching the exception at all. And for precondition violations, something like assert() is recommended instead. I believe the practical result is that obstructions to an operation are managed with something like error codes, and violations of an assumption may trip assert()s or exceptions
  • JavaScript and Clojure technically both have exceptions and try/catch, but I think really only for legacy reasons, in practice obstructions to an operation are managed with error values and such
  • the practical result, I think, is that exceptions in C++, JavaScript, and Clojure are kind of like panic!() in Rust: you try to avoid causing any at all, you only use them in places you think are unreachable, you don't bother trying to recover from them if they do happen, but in case they do indeed happen, you do code defensively to try to crash gracefully by cleaning things up in destructors and try/finallys. (The closest analogy in C is just crashing the process)
  • good:
    • once you're used to it, it's fairly clear when to return an error value vs throw an exception: if somewhere is unreachable (or you want to fail fast, like something unimplemented), you can throw an exception, otherwise if you want to notify about an obstruction to the operation, use an error value
    • it's also fairly clear when to handle an exception: don't, other than cleaning things up to attempt to crash gracefully
    • it couldn't be clearer whether it's your responsibility to handle a returned error value because unlike exceptions, they don't go up the stack to find someone else to bother if you ignore them. You either drop them or you handle them
  • bad:
    • JavaScript in particular has a bit of a "worst-of-all-worlds" problem:
      • the try/finally footguns badly need a try-with-resources statements (there's a TC39 proposal for a try using() statement)
      • the happy path is littered with error-handling early-return noise due to lack of language support
      • the early returns have another version of the try/finally resource cleanup problem, unless you use try/finally in the right way there too
      • (I'm not sure how much this applies to C++, which uses destructors to handle resource cleanup automatically when the stack unwinds, or Clojure, which I suspect has alternate patterns with similar effect to Python's with statement, similar to Ruby)
    • neither error codes/values nor exceptions are statically checked at all, and can be a little too easy to ignore
    • not only is there little language support, the presence of throw/catch in the language almost seems like it's encouraging Java or Python-style error handling. This can be exacerbated by low-effort language tutorials that try to "comprehensively" cover every language construct, instead of teaching how the language is/should be actually used in practice

• return error values, with language support: Haskell, PureScript, Scala, Rust, Elm (a little)

  • every Haskell tutorial proudly touts the monadic Maybe and Either types, which eliminate unhandled runtime exceptions, especially NullPointerExceptions, and monadic do-notation lets you use them in apparent "direct style".

    • However, I think this is actually only ergonomic for extremely localized error handling within pure functions. Mixing monads, like mixing code that has side-effects with Maybe or Either, is notoriously painful
    • Haskell ultimately compromises on purity anyway, allowing even pure functions to be "partial" and throw errors with error. They can only be caught in the IO monad, although like JavaScript exceptions or Rust panic!(), you don't normally want to catch them anyway
    • there are also several additional ways to manage errors, for added confusion (some have been unified or deprecated), all for Haskell-specific problems (lazy evaluation or more monad problems)
    PureScript and Scala appear to be in basically the same boat as Haskell

    • PureScript very similar to Haskell down to the do-notation, although it is strictly evaluated rather than lazy. (It used to be more different with its row-typed algebraic effect system, but apparently that had enough problems that they switched to an equivalent of Haskell's IO monad)
    • Scala appears to treat its unchecked JVM exceptions much like Clojure (and much like JavaScript exceptions and Rust's panic!()). Recoverable errors/obstructions to the operation are instead meant to be handled with its Option and Try types, analogous to Haskell's Maybe and Either (although Scala also has an Either type for good measure), which you can pattern-match on. You can even use for comprehensions to monadically code in a sort-of "direct style", although I think the syntax is weird when used that way and I don't know if anyone but the people obsessed with contorting Scala into functional programming idioms do that

  • Rust also takes significant inspiration from Haskell, with pattern-matching and Option and Result types analogous to Maybe and Either for obstructions to an operation, and runtime panic!() for violations of an assumption.

    • Rust does one better than Haskell though: instead of do-notation, the ? operator is specialized to Option and Result and makes it easy to short-circuit upon None or Err, while still forcing the programmer to have to choose to do so

  • Elm is like Haskell but without do-notation, or any replacement, really. Pattern-match or bust

  • good:

    • runtime errors are rare in practice without serious misuse of error/panic!()
    • unhandled errors are technically impossible due to typechecking, although that can't prevent misuse of error/panic!() of course
    • Rust's ? operator is brilliant in my opinion. A bit of friction to ensure it's impossible to forget to handle an error, but minimal friction, it's just one character
    • I think with the "obstruction to an operation" vs "violation of an assumption" framework, it's pretty easy to see when to use Result and when to panic!()

  • bad:

    • I'm not sure how much thought has been put into the try/finally usability problem. Haskell and PureScript as a functional languages aren't really supposed to error ever (I think Clojure has this attitude as well); Elm as a frontend language isn't usually used for a lot of resource management. No idea about Scala.
      • Rust destructors, like C++, are tied to function stack frames, so they should work fine with panic!() stack-unwinding or early-returns on error. Some panics abort the process instead of unwinding the stack, but I guess in those cases it's the OS's problem
    • forced handling of errors can be annoying, especially if it's obvious to the programmer they're actually impossible; in Haskell and Rust that leads to fromJust/.unwrap() littering the code, in Elm doesn't even give you that option, you're supposed to just pattern-match anyway

• oddities: Go, Erlang

  • Go's error handling gets a lot of hate, which I think is mainly because errors are checked (the compiler complains about unhandled errors), but there's no sugar for either early-return-on-error or panic-on-error, so it feels like you're writing a lot of boilerplate—that blogpost is about writing your own such sugar, which seems like kinda missing the point. I think Go pioneered the defer statement, though, which I do think was brilliant, and was copied by Swift and Zig.

    I'm not sure which I like more, the `defer` statement or Python's `with` statement (aka `try`-with-resources)

    • API design
      • with makes it a little easier to design an API that's difficult to misuse, like instead of returning a file object you could return a context object that you have to enter in order to use the file
      • the problem isn't people forgetting to call file.close() at all, the problem is people thinking they called it correctly when actually they nested try/finally subtly incorrectly, which defer solves
    • readability
      • with is a little more readable, there's slightly less code because you don't have to explicitly call .close(), it's implicit
      • defer doesn't introduce additional indentation, whereas with can be unpredictable: you can enter two contexts with one with statement, but what if you wanted to do something in between entering the two contexts?
    • flexibility
      • with is highly flexible, you can even simulate defer with ExitStack(), such as to reduce indentation
      • basic usage of defer is more flexible though, you don't have to bother with something that implements a "context manager" interface, just run a line of code out-of-order

    On balance, I think I prefer defer. As long as Mechanical doesn't have control flow, though, it doesn't really matter.

  • systems written in Erlang are famous for their uptime, and a big part of that is error recovery, but not really in the sense discussed here. Erlang is unusual in many ways—no mutable data or variables (like Haskell), but dynamically typed (like Lisp)—but its control flow is actually fairly mainstream, with exceptions that unwind the stack and try/catch/after for catching them. As far as I can tell, Erlang has nothing like defer or try-with-resources.

    • Erlang's famous reliability isn't due to the localized, fine-grained exception handling, but rather due to the coarse-grained error handling and recovery at "process" boundaries—in Erlang, it's customary to create lots of green threads, which Erlang calls "processes" because they don't share a namespace. Processes are organized into "supervisor trees", so that when processes encounter an error, instead of worrying about recovery from it, it can exit and let its supervisor restart it.
    • This leads to the philosophy of Let It Crash: "only program the happy case, what the specification says the task is supposed to do". Doing lots of fine-grained error handling in an attempt to code "defensively" and be "robust" is actually counter-productive. Instead, when surprising stuff happens, just let it crash, and put your effort into designing an overall system architecture that is robust to surprises in the first place.
    • Or to put this in terms of "obstructions" and "assumption violations", this of course doesn't mean you should crash in response to any and every predictable obstruction to an operation. Predictable obstructions should be considered in the specification and handled sensibly. But it's counter-productive to try to code defensively by making fewer assumption than the spec, instead you shouldn't be afraid to make assumptions and crash when they're violated.

• Swift, Zig, Go sort of (it has defer)---return-oriented with more thought put into it

The biggest inspiration for Mechanical's error handling is Zig, Swift, and Rust, with lessons from Haskell, Go, Python, and of course, JavaScript and Java.

SMT_and_Mechanical.md

(WIP) Thoughts on SMT solvers, theorem provers, proof assistants, and Mechanical

Background and Motivation: Type narrowing for less painful error handling

So a is an array of strings and i is an integer. What is the type of a[i]? We want it to be a string, but what if i is out-of-bounds?

In most languages, the compiler can safely assume the return value of a[i] will be a string because if i is out-of-bounds, no value will be returned, instead an exception will be thrown. Even Haskell does this. (In unsafe type systems like C or TypeScript, the compiler can't safely assume that, but assumes it anyway.)

I want Mechanical to be strictly typed, I don't want unsafe assumptions, but I also don't want control flow like throwing exceptions. The current plan is to return an #error #out_of_bounds error value, but unfortunately, that means in general the type of a[i] is string | #error #out_of_bounds. This is similar to how Haskell/ML/Elm/Rust's Maybe/Option and Result/Either types are used for error handling, but for something as common as array or list access, most such languages consider it to be too much of a pain to force the programmer to explicitly handle the error case every time. (Notable exceptions I know of are Elm and PureScript, which are both compile-to-JavaScript languages, coincidence? Is it less of a pain in typical Node.js or browser code?)

You know what's weird, though? Usually, the programmer has already written their code in a way that guarantees the array access will be in-bounds. So if they've guaranteed the error case can't happen, then why are we forcing them to handle the error case at all?

What if the compiler attempts to infer whether the programmer has indeed correctly guaranteed that the array access will be in-bounds, and if so, it uses type narrowing to eliminate the #error #out_of_bounds from the return type in the first place? This is where SMT solvers come in.

Solver Design

situations range from obvs true, all the way to easy counterexample

in the middle, it's hard to know, goal of these systems is to determine which

they can either spend CPU time and engineering effort on seeking out counterexamples, or in trying to reason out correctness

more effort seems spent on former; maybe easier? Because it's just re-ordering the trial-and-error search?

But we would rather trade it off for latter, because we assume programmer smarter than computer

specifically, that programmer understands their code better than a compiler with very limited time budge will

a model checker that runs on CI or something might make the opposite tradeoff

Appendix: Other pieces of the error handling puzzle

I can think of basically three approaches to addressing this ergonomic problem:

• one approach, somewhat silly in my opinion, is to make common problematic functions total: a[i] is actually a[i % a.length] (pretending % means modulus like in Python, rather than remainder like C/C++/Java/JS); integer division by zero returns zero.
  • Surprisingly to me, several languages/environments obsessed with mathematical purity specifically define division by zero to return zero, like Coq, Isabelle, and Lean, which are all automated theorem provers/proof assistants, as well as Elm and Pony (extended discussion). That's not what Coq does about indexed vector access, though
• another approach is make the ergonomics of dealing with error values more similar to thrown exceptions, like JavaScript's optional chaining operator ?., Rust's ? operator for error propagation, or even Zig's error return traces. It's easy to design these for pure code (everything is easy with pure code), but how do these interact with commands and Do statements, considering Mechanical is a concurrent language without conventional control flow?
• finally, we can take inspiration from the classic Ghost of Departed Proofs (GDP) paper: usually, the programmer has written their code in a way that guarantees the array access will be in-bounds. So if they've guaranteed the error case can't happen, then why are we forcing them to handle the error case?
  • Obvious answer: because the compiler can't tell whether or not the programmer has indeed correctly guaranteed that the array access will be in-bounds.
    • Coq, Agda, Idris solve this problem by requiring the programmer to provide highly specific type annotations, much more specific than possible in conventional type systems, specific enough that the compiler can safely check that the array access will be in-bounds. This is only possible because of a powerful feature called dependent types, and it comes at a big price: these languages require a lot of manual type annotation by the programmer, and because the types are more specific, you have to think harder when writing them, too. (It's a classic easy-to-verify, hard-to-solve problem: the compiler can verify whether your annotations are right, or at least consistent with each other and array bounds and such, but can't on its own figure out what the correct annotations are supposed to be.)
    • GDP is in Haskell, which doesn't have dependent types (yet). Instead, similar information is cleverly encoded into Haskell's type system, which isn't quite as safe (not as strictly checked by the compiler), although it is more flexible. The ergonomics aren't great, though; the annotation burden isn't much better than dependent types, and being hacked into the language means the error messages are pretty garbled.
    • A sort of "compromise" approach is refinement types. These are more restricted than dependent types, in return for being amenable to inference using cutting-edge SMT solvers, while still being specific enough for may useful things like array bounds checking. However, state-of-the-art SMT have unpredictable runtimes, since they attempt to use heuristics to solve often NP-complete problems. Also, in practice, refinement types still seem to require a few type annotations (though much fewer than dependent types), and I'd prefer if Mechanical had no type annotations whatsoever.
  • So the idea of this note is that if Mechanical can efficiently infer especially-weak refinement types, and thereby safely verify that an array access is in-bounds, it should be able to use type narrowing to eliminate the #error #out_of_bounds from the return type in the first place.

Of course, given all the limitations I want to impose (reliably linear time, no annotations), refinement type inference and narrowing will clearly be an incomplete solution, and I will need some combination of the other approaches, too.