Ancestors

Toot

Written by gigapixel on 2024-12-30 at 09:15

Something that’s been on my mind as one of the key benefits of theorem provers like #leanlang #Lean4 for someone like me is they enable storing reasoning long term much more effectively than written proofs as well as forcing local reasoning.

I left academic #math about 8 years ago to have a more stable and less demanding career in tech. But I always intended to continue my research in an informal capacity, just for love of the subject. I managed to do a halfway decent job as well, but the big problem is that I would work on my math maybe once or twice a week. And here I found that I would always lose an inordinate amount of time with context switching. My work style until that point had been to develop a complete sketch proof and fill in the details. Importantly this required me to always maintain a sort of complete picture of the proof in my head. But now being unable to focus full time on cleaning up the sketch I would lose so much time trying to remember the notation that I created as well as reloading the whole strategy.

My time in tech has exposed me to a bunch of programming languages. At first Python which sort of fit with this sloppy idea of just keeping the whole program in my had with a lot of global variables. But bit by bit I was exposed to other more rigorous languages: first #scala and then #rust #rustlang . It was really in rust that I started to get the idea of local reasoning.

Especially rustlang folks seemed interested in formal methods and bit by bit I got exposed to those languages through them.

Now especially with “sorry” I can incrementally work on goals with consistent notation and without having to load the full context as the intermediate goal is right there.

=> More informations about this toot | More toots from gigapixel@mathstodon.xyz

Descendants

Written by gigapixel on 2024-12-30 at 09:35

One of the big potential synergies between #rust and #lean4 rely on the rust type system which is sound (https://en.m.wikipedia.org/wiki/Type_safety). I have a long ongoing project proving liveness properties for a collection of parallel and concurrent #stream processing combinators. Rust’s type system should allow guaranteeing liveness for these combinators at compile time. But it is not rich enough to prove liveness in the first place. And that’s one reason I got interested in lean. Other languages crossed my mind like #rocq (formerly #coq) and #tla_plus but lean won out for its rich math library, connections to the #math community, and great tooling (like nvim integration).

=> More informations about this toot | More toots from gigapixel@mathstodon.xyz