applications of ITPs in computer science

Stream: general

[Kevin Buzzard]

Hopefully an easy one for some of our readers: I am giving a talk to undergraduate computer scientists in Oxford and I wanted to do just a few lines on applications of ITPs in computer science; so far I have one line: "there is a formally verified kernel and a formally verified C compiler". Is that a short but accurate summary of the main achievements of ITPs in the area of "checking code has no bugs" (let me stress that "checking code has no bugs" is going to be 1 slide of my talk max, I'm talking mostly about SOTA with LLMs + ITPs doing mathematics)

[Siddhartha Gadgil]

A striking example is the story of TimSort (my slides on this at https://siddhartha-gadgil.github.io/presentations/o9CompProofAI.html#/11).

[Siddhartha Gadgil]

To save googling, the source is http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/

[Marc Huisinga]

I'm not sure to which degree KeY counts as an ITP, though

[Jannis Limperg]

There's a lot more. Some high-visibility projects off the top of my head:

• Evercrypt: verified crypto routines used in Firefox, Linux kernel, ...
• Rustbelt: verification of Rust's type system, including unsafe blocks
• CakeML/Candle: verified Standard ML compiler and HOL Light-style ITP

[Joachim Breitner]

Evercrypt is a nice example because (anecdotically) it's faster than a manual implementation, because when it's all verified you can do optimization stunts that you wouldn't dare otherwise. But I should probably find a citation before spreading such rumors :-)

[Kevin Buzzard]

How far is Rustbelt from "it's possible to verify (in some sense) that simple rust programs are correct"? Is this still a dream away or has this already happened? I know that people can start going on about trusting compilers, chipsets etc etc but I'm talking about something which looks like it's doing the job of proving that an explicit simple program has no bugs. I tried looking at the project webpage but it's all way over my head.

[Shreyas Srinivas]

sel4 the os kernel

[Kevin Buzzard]

yeah, that and compcert are the two I knew about already (see original post).

[Shreyas Srinivas]

Kevin Buzzard said:

How far is Rustbelt from "it's possible to verify (in some sense) that simple rust programs are correct"? Is this still a dream away or has this already happened? I know that people can start going on about trusting compilers, chipsets etc etc but I'm talking about something which looks like it's doing the job of proving that an explicit simple program has no bugs. I tried looking at the project webpage but it's all way over my head.

I am attending Derek's lecture now. I'll ask and let you know

[Shreyas Srinivas]

There is also Dargent

[Shreyas Srinivas]

There is the fully formal verification of kyber

[Kevin Buzzard]

There is also Dargent

took me to "Coq d'Argent" which sounded promising but turned out to be a restaurant in London.

[Shreyas Srinivas]

Not coq

[Shreyas Srinivas]

Isabelle

[Shreyas Srinivas]

Christine Rizkallah et al.

[Shreyas Srinivas]

There are some successes with synthesis too. Check Ilya Sergey's PLDI paper from this year

[Shreyas Srinivas]

Kevin Buzzard said:

There is also Dargent

took me to "Coq d'Argent" which sounded promising but turned out to be a restaurant in London.

https://dl.acm.org/doi/abs/10.1145/3571240

[Shreyas Srinivas]

Fancy Post Quantum Crypto stuff: https://eprint.iacr.org/2023/215

[Karl Palmskog]

proven-correct C code for cryptography generated by Fiat Crypto (Coq library/tool) was integrated into the BoringSSL library used by the Chrome browser

[Leo Stefanesco]

Kevin Buzzard said:

How far is Rustbelt from "it's possible to verify (in some sense) that simple rust programs are correct"?

The original paper has some simple examples, and an unpublished paper has some examples proved using automation on top of Rust Belt.

[Yaël Dillies]

Siddhartha Gadgil said:

A striking example is the story of TimSort (my slides on this at https://siddhartha-gadgil.github.io/presentations/o9CompProofAI.html#/11).

Does this have to do with Vincent Jugé's work somehow?

[Kevin Buzzard]

Does python have a spec? Do people work on questions such "assume python conforms to its spec. Then the following code has no bugs"?

[Shreyas Srinivas]

The answer from Derek was that rustbelt was focussed on proving the safety of rust APIs where it was non trivial to establish such properties. The work to scale those to full programs with suitable automation is ongoing

[Jason Rute]

I think someone verified Scala’s type system in Coq to make sure it was correct.

[Shreyas Srinivas]

But he also said that they have infact verified "non-trivial" programs for some suitable definition of non-triviality.

[Jannis Limperg]

Kevin Buzzard said:

Does python have a spec? Do people work on questions such "assume python conforms to its spec. Then the following code has no bugs"?

I'm not aware of any work on Python specifically. People tend to focus on C (because that's what safety-critical applications actually use) or functional languages (because they're nice).

[Jason Rute]

I think Java also has a specification, but I’m not an expert. I get the impression that Python is really hard to specify.

[Shreyas Srinivas]

I just realized that you might potentially not have come across the common intro line for ITP papers in CS . It is usually some variant of

"Model checkers and sat solvers might allow you to verify complex properties automatically, but they suffer from two problems: State space explosion, and the need to contort the spec to fit the decidability and complexity limits of the model checkers. ITPs overcome these issues and allow us to express specs more naturally at the cost of manual proving". This is a semi-correct claim that I have seen in enough paper intros to remember it.

[Shreyas Srinivas]

Semi-correct because you can certainly generate super large terms for the type checker to check, and ITP users do have the challenge of picking the right fornalism for their definitions and theorems, to simplify proofs

[Timo Carlin-Burns]

Wasn't this paper a spec for Python? https://cs.brown.edu/~sk/Publications/Papers/Published/pmmwplck-python-full-monty/

[Wrenna Robson]

There's very exciting work that uses EasyCrypt and Jasmin together to produce verifiably secure and correct fast assembly implementations

[Wrenna Robson]

https://blog.cloudflare.com/post-quantum-easycrypt-jasmin/

[Wrenna Robson]

This is an accessible post on the subject that cites close to current literature

[Wrenna Robson]

EasyCrypt in particular is essentially a specialised ITP I believe

[Wrenna Robson]

I have myself used Galois's Cryptol/SAW toolchain in the past and it is good though not I think the focus of their current work. I think they are currently doing some stuff with Coq (they were looking at Lean but I think that dalliance petered out). Galois do good work in this area in general.

[Karl Palmskog]

Jason Rute said:

I think someone verified Scala’s type system in Coq to make sure it was correct.

There is a formalization in Coq of Scala's foundation, the DOT calculus, here:https://github.com/Blaisorblade/dot-iris