I found a cool paper that seemed relevant for discussing error handling! https://www.cs.cornell.edu/andru/papers/ufo/
Gosh, I feel like the algebraic effects literature is rediscovering call/cc all over again. At some point someone is going to point out that complex control flow is complex
In fairness, Rust is definitely an exercise in applying 40 year old technology, so while I agree, I also can't really hold that against them. :^)
Coq I think could certainly be described as 'comprehensive'
oh this is sick
I've been wanting to read about this kinda thing for a while
thanks for pointing it out @Jubilee
Oh if you're interested I usually don't like spamming theory papers but here is one
that just came across my desk and has some formalism around bidirection:
Seems alright to start I haven't read it all
my brain is roiling with thoughts about effect handlers enabling computational expressions a la F#.
isn't that what the backtrace does?
or rather the call to render the backtrace
https://docs.microsoft.com/en-us/dotnet/fsharp/language-reference/computation-expressions the thing I'm thinking of is this, where basically you can define-your-own-syntax for "async" or "try" blocks.
the prototype we have now is
write_backtrace_to(&mut dyn FormatterThing) -> Result<(),FormatterThing::Error>
there is talk about shimming (my word) in some try syntax
Last updated: Jan 26 2022 at 14:20 UTC