Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point.

My PhD is in regards to proving properties about robotics, so maybe in 5-6 years I'll have fully bridged industry and theory, but I wouldn't hold my breath :)

[1] https://www.fstar-lang.org/

Theorem-proving gets some use in the Ethereum community. Smart contracts are an ideal application for it: the code is short and bugs can be disastrous.

> Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point.

As someone who doesn't code for a living, I am certain that this is a naïve question, but, if you want to use theorem-proving software for verification of existing code, does that require employer permission? Is the issue something like, e.g., you need the theorem-proving software and the code to be verified on the same machine, and you're not allowed to install the theorem-proving software on a work machine or to move the code to a non-work machine?

I meant that I couldn't get budget to do it. Obviously I could do a code verification in my free time, but my goal was to start the project with everything that could be written in FStar being written in FStar, with my coworkers onboard.

I had root access to my laptop so I could install anything I wanted, but it's hard to do anything if you don't have budget allocated to do so.

EDIT: I also should point out that I wanted to export the code from FStar to F# and use the exported and verified code.

I work on a project that is 20 million lines of code - while large someone reading this is working on a project much larger. There is no way any human working alone can prove the whole thing. I have no idea how to even get started. Even if I did, until I can prove theorem proving is useful in the real world I'm stuck doing it as a side project: my boss will encourage it, but if I spend no more than a couple hours a week one it

Now in my company we are worried about bugs and reliability. If I can show via example that theorem proving catches bugs they will train all developers on it and demand all code be proved. However proving quality needs to be something that is worth the effort, if it slightly increases quality but at the expense of making projects take 10 times as long it is probably not worth it except for specific areas of concern.

I feel like it's much harder to shoehorn in proofs to existing codebases than it is to start with the proofs first.

The automation in Isabelle is quite good; good enough to where I don't feel that writing pure new code with proofs takes me a prohibitively long amount of time (about 2-3x writing the equivalent Haskell) (sledgehammer ftw), but I can't imagine trying to retroactively go and prove any of my old projects that are considerably smaller than 20 million lines.

One big perk for using Isabelle (or other proof systems), outside of the obvious correctness proofs, is being able to prove equivalence. If you can inductively show that two functions have the same inputs and outputs (say one was quick to write or easy to prove things about, the other is efficient), then you can tell the code exporter to replace any instances of the inefficient version with the efficient version. This means that your optimization is proven safe, and is done for free, which is worth its weight in gold when used correctly.

Of course, this really only applies to pure and mathey functions. It's substantially harder to prove properties about business logic.

> I feel like it's much harder to shoehorn in proofs to existing codebases than it is to start with the proofs first.

This is one of the big problems in CS. We have code that has been in production for 20 years and as such has very few bugs left. We know from experience replacing that code with new proven correct code results in something more buggy (for a few years while we fix the incorrect requirements) than the original. We still are replacing a lot of old code with proven correct code, but only as the CPU it is tied to goes out of production (code that is portable thus is low on the to replace list). If we could prove existing code correct easily it would potentially save a lot of money as we can keep old code around and add correct features.

> We have code that has been in production for 20 years and as such has very few bugs left.

That seems optimistic!