Do people use proofs in "normal" programming?

Stream: new members

[Dan Abramov]

Since Lean is a runnable language, I'm wondering if anyone is using (or experimenting with using) it in a following fashion: writing "normal" (not like super academic) runnable programs but with some properties being passed around as proofs.

I know obviously people use Lean for proving mathematical theorems, or proving some statements about some systems (maybe some algorithms we want to model). And I know you can also write runtime code in Lean. So what I'm curious about is more like, do these get interleaved. Like would you write a web server with some proofs being passed around right in the midst of it. Or some other general purpose software that has no (obvious) connection with mathematics or formal systems.

[Aaron Liu]

I do it to avoid bounds checks

[Aaron Liu]

yea in regular programs too if it's not too much hassle

[Dan Abramov]

That seems like the most obvious use case, Claude suggested this to me too. Which feels like the most "practical" and "boring" application at the same time, but maybe also easiest to appreciate coming from TS etc. I wonder if that evolves into something bigger or whether that's too much effort. Or how does it influence how you think about other aspects of the program.

[Dan Abramov]

Like I guess I'd maybe reach for proving some properties about things where I'd previously reach for tests? For critical pieces. And then maybe more relaxed in other places but using properties here and there. Or having them be a part of the design of how different parts "fit in", like maybe security things like proving user input was escaped.

[Aaron Liu]

Just today I was passing around an term with type { n : Nat // xs.length = n } and this turned my quadratic time algorithm into linear time without having to make the matching more complicated since the cases where the list is empty and the number is positive and the one where the list is nonempty and the number is zero were eliminated automatically

[Dan Abramov]

Ah yea I love this, so safe more aggressive optimizations.

[Kyle Miller]

I've used structures that contain the invariants that the fields are supposed to satisfy, which helped me think about the algorithms I was writing. I actually proved some of them, but other parts I left as sorry when I was confident it was ok (maybe more accurately: when it would have been a lot of work to fill in a formal proof!)

It's interesting, when writing programs passing proofs around is sort of like strong typing++, where you use the more sophisticated types to make sure things are glued together in a way that prevents data model errors, but when writing algorithms where the goal is to prove correctness, it seems like it's often better to not pass proofs around, but instead write the algorithm and then leave the proofs for the theorems about the definition.

The example of array bounds checking is a good one. When writing programs, yeah, it's helpful to know that you've got the basic correctness of not indexing out of bounds. But if you're writing theorems, you may as well write everything with arr[i]! since once you prove the program meets its spec you basically know the array indexing must have been in bounds. Using arr[i]! also avoids the dependent types in arr[i]'h (h depends on both arr and i), so it's easier to rewrite arr and i. I say "may as well", but to be clear that's not a recommendation, you also may as well prove indexing is in bounds inline if it's easy enough to do :-)

[Rado Kirov]

Just today I was passing around an term with type { n : Nat // xs.length = n } and this turned my quadratic time algorithm into linear time

@Aaron Liu is this in a github repo that we can see? How did you know the compiler is making proper use of the extra type info?

[Rado Kirov]

Array bound is a good example for TS devs, because JS runtime doesn't crash on out-of-bound access but just returns undefined. Because TS type system is not expressive enough to carry array size information and number range information statically, TS basically has to pick between two bad choices a[i] on a: T[] should always return either T or T|undefined (can't express that this choice is dependent on i which it truly is. They recently made this configurable through noUncheckedIndexedAccess but it is not on by default in the recommended strict flags, because of how unergonomic it is to deal with | undefined even for a simple for loop.

[Markus Himmel]

In the self-balancing binary search tree implementation in the standard library, we use proofs of balancing properties to show that certain situations cannot occur during rebalancing. This allows the compiler to remove the corresponding branch entirely, unlike in e.g., Haskell, where you would need to check and then panic in this situation. The speedup from this is quite noticeable in our microbenchmarks.

[pandaman]

I tend to avoid writing proofs in programs unless necessary. For example, I'd happily add a bounds check for ordinary functions, while I pass an in-bounds proofs to the hot loop.

The issue is that the proofs obscure the implementation, especially in a recursive function when you need to prove the properties for the new arguments. I once wrote a function where the proof in it was twice as long as the actual data manipulation :joy:

[Aaron Liu]

Rado Kirov said:

Just today I was passing around an term with type { n : Nat // xs.length = n } and this turned my quadratic time algorithm into linear time

Aaron Liu is this in a github repo that we can see? How did you know the compiler is making proper use of the extra type info?

I don't think the compiler is doing anything with it, since subtypes are represented the same as types in the runtime. It saved me two match branches, and it saved me recomputing the length of the array at every recursive call since I'm passing it down now. Eventually I optimized it out.

[Tyler Josephson ⚛️]

We're writing code for scientific computing applications in Lean, and have been integrating proofs with programs in a way that makes sense to us. We're not passing proofs around with functions, nor do the proofs really impact speed or performance - the proofs are there to verify properties of the functions we're executing.

[Arthur Paulino]

You might be interested in this implementation of squeeze, for which I was able to provide a proof for the size of the output.

Btw, I think ByteArray.size_of_extract would be very useful in Batteries.

[Arthur Paulino]

As already mentioned in this thread, it's common (and often good) practice to add runtime assertions for bounds of arrays/vectors/slices of data. If you can lift those runtime bound checks to compile-time proofs, your application is not only safer but also faster.

[GasStationManager]

I use the interleaving style extensively in my attempts to get AIs to write code with correctness proofs. See here for some examples. It is often the only way I could get Claude to make progress on the proof. In my opinion it is the most intuitive approach if the goal is to produce code with a correctness proof: you can think of the code as already the proof sketch. Why would you want to then unfold the function from outside in order to fill in the rest of the proof. Granted, the end result might not be the most readable, but readability was not the goal.

[pandaman]

Because I want to prove five theorems about a definition, but I don't want to interleave it with five proofs with different induction hypothesis! Readability matters to me.

[Alok Singh]

I have some in github.com/alok/lean-inf (currently broken though). I found them invaluable as glue for AI models too since even with everything sorried they still act like legos for snapping types together.