Abandonment in "Lean as a normal programming language"

Stream: general

[Owen Lynch]

When using Lean as "just an improved Haskell", I wish that I could "abandon" when I detect a bug, in the sense of https://joeduffyblog.com/2016/02/07/the-error-model/#bugs-arent-recoverable-errors.

The advantage to abandonment as opposed to returning Option a is that it gives me a good stack trace that I can use to start debugging. Is there a way of doing this in lean? So far what I've seen requires the return type to implement Inhabited.

[Owen Lynch]

Perhaps the solution would be to have something like a typeclass MonadPanic which could be used for code whose correctness is not yet proved, and which intends to abandon on bug detection.

[Owen Lynch]

In a similar vein, are there projects to get Dafny-style program verification in Lean? It would be useful to have a "gradual typing" approach to program verification, where one can choose to dynamically assert conditions which are not yet proven to hold.

[Aaron Liu]

Owen Lynch said:

Perhaps the solution would be to have something like a typeclass MonadPanic which could be used for code whose correctness is not yet proved, and which intends to abandon on bug detection.

We have docs#Alternative which gives you recoverable errors

[Aaron Liu]

We have docs#MonadExcept which gives you catchable errors

[Aaron Liu]

I unfortunately don't see any "monad unrecoverable error"

[Aaron Liu]

but if your monad implements Inhabited then you can just use panic!

[Kyle Miller]

Lean has panic! to abandon a computation

[Kyle Miller]

You can also use if h : p then ... else panic! "error" for getting access to a proof of h in the success branch.

[Eric Wieser]

It doesn't actually abandon though unless you set the right environment variable

[Patrick Massot]

Owen Lynch said:

In a similar vein, are there projects to get Dafny-style program verification in Lean? It would be useful to have a "gradual typing" approach to program verification, where one can choose to dynamically assert conditions which are not yet proven to hold.

Have you seen #Program verification > Monadic program logic: Request for feedback @ 💬 already?

[Paul Biberstein]

What environment variable do you need to set to abort on panics? Coming from Rust, I found it quite unintuitive that panics don't kill the process.

[Paul Biberstein]

Nevermind, see this discussion #general > lean 4 and panics

[Owen Lynch]

Aaron Liu said:

but if your monad implements Inhabited then you can just use panic!

Ah, this is perhaps the most reasonable strategy: it's annoying to have to make all of my types Inhabited, but it is a good idea to make the monad implement Inhabited. Especially because I'm already using MonadExcept Unit for expected kinds of errors.

[Owen Lynch]

Patrick Massot said:

Owen Lynch said:

In a similar vein, are there projects to get Dafny-style program verification in Lean? It would be useful to have a "gradual typing" approach to program verification, where one can choose to dynamically assert conditions which are not yet proven to hold.

Have you seen #Program verification > Monadic program logic: Request for feedback @ 💬 already?

This looks quite cool!

[Kyle Miller]

Owen Lynch said:

it's annoying to have to make all of my types Inhabited

Are you using deriving Inhabited?