Master program advice

Stream: general

[Augusto Hack]

Hey there. I want to do a master to get my hands dirty with automated provers, I wonder if anybody has some advice on programs I should look into. I'm currently based on Berlin/DE and it seems that Munich/Saarbrucken would be better options for this subject (or maybe even UK/SE). I know this is broad question/hard to answer but any advice helps. Thanks!

[Jasmin Blanchette]

Our field is quite small, you won't find a "theorem proving" MSc program anywhere I'd think. Ultimately, doing a MSc is mostly about finding the right supervisor and topic, and maybe taking one course on the topic, like Concrete Semantics at the TUM or Automated Reasoning I and II in Saarbrücken. Christoph Benzmüller may also be teaching such a course at FU Berlin.

A very important, early decision is whether you are more interested in interactive or automatic theorem proving.

[Kevin Buzzard]

Another question is whether you're more interested in the mathematical side of things or stuff like program verification (you can prove theorems in maths and you can prove theorems about computer programs). The basics of the two areas are the same but then at some point divergence occurs

[Augusto Hack]

I'm definitely more interested in program verification side of things, and I suppose interactive theorem proving. I'm actually more interested in applying the existing techniques than expanding the state-of-art. My experience is more as a distribute systems engineer and I would really like to see the existing techniques applied to reduce bugs. I prefer to spend a week proving that a system is correct under a model, instead of spending a month chasing a consistency bug. My idea was to get into a master program to get more proficient with the existing ecosystem and then try apply it to my daily job.

[Jannis Limperg]

That's a worthy goal but your timelines are flipped: you'll more likely spend a year proving your system correct (unless your system is extremely small or you manage to find a mostly-automated prover that fits your system's needs). Interactive theorem proving is, for now, a very laborious process. With that said, there are certainly people working towards industry-ready tools, so I don't want to discourage you too much.

[Chris B]

@Jannis Limperg
This doesn't contradict any of what you said, but just to add a dash of optimism in the realm of verification in industry (with the caveat that the source is not entirely neutral), Gernot Heiser claims that the the development costs of seL4 were much lower than those of other high-assurance software using traditional methods; $400/loc compared to $1000/loc.

[Kevin Buzzard]

But is seL4 actually usable in practice?

[Pedro Minicz]

Kevin Buzzard said:

But is seL4 actually usable in practice?

Yes, it should be. I don't know about seL4 specifically, but kernels of the L4 family are widely used in tiny embedded systems. Your smartphone probably has a microprocessor running L4 to mediate the communication between the mobile network and the phone's CPU.

[Kevin Buzzard]

But the version my smartphone is using isn't formally verified, right?

[Pedro Minicz]

Right, it is not formally verified.

[Joe Hendrix]

To answer @Augusto Hack original query, for distributed systems verification, this question came up at Galois recently, and the recommendation was to pick a particular system that you know well, modeling it in TLA+ and trying to verify some properties using TLC.

[Joe Hendrix]

I'm not sure what the masters programs in Germany or UK at like, but I think in the US at least, a master's program is a pretty inefficient way to get practical experience using FM tools. A master's or PhD program is much more important if you want to contribute on the research side or build up fundamental mathematical skills.

[Joe Hendrix]

If you want something more powerful and requiring more expertise than TLC, Ivy would make a good other system to learn. Lean is great if you want a general programming language that also has verification capabilities, but isn't explicitly designed for distributed systems verification. It's also great as a way to learn dependent types.

[Jannis Limperg]

Chris B said:

Jannis Limperg
This doesn't contradict any of what you said, but just to add a dash of optimism in the realm of verification in industry (with the caveat that the source is not entirely neutral), Gernot Heiser claims that the the development costs of seL4 were much lower than those of other high-assurance software using traditional methods; $400/loc compared to $1000/loc.

That's an interesting number, thanks!

[Joe Hendrix]

I'm really skeptical of numbers like that personally. I'd want to know by "other high-assurance software", and how those numbers were computed. Costs in "high assurance software" are likely heavily influenced by the costs of certification and accreditation. SeL4 would still have to pay those costs since no certification process I know let's one use FM to just skip certification requirements.

[Ryan Lahfa]

In Paris, you have the MPRI, which has a wide choice of subjects including type theory, automated deduction and proof assistant: https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:cours2 ; I'm not sure that it gets that much in-depth as real experience using tooling yourself. But from a research standpoint, I heard it was good, AFAIK, some people from Coq teach there.

[Chris B]

There's some more detail about development costs starting on page 6 in this paper if you're interested. https://sel4.systems/Info/Docs/GD-NICTA-whitepaper.pdf
In a talk at linuxconf, Heiser attributes the $1,000/loc number to a report by Green Hills Software.

[Chris B]

Granted that's also a sales-pitch, so I wouldn't deign to call your skepticism unhealthy.

[Joe Hendrix]

Thanks. I don't disagree that much with the idea that FM can produce software at prices not all that different from traditional assurance.
On the other, I'd guess the $1000/loc for INTEGRITY also includes DO-178A certification which seL4 does not have. INTEGRITY is older, and I think Rockwell was involved in it's design and implementation. My limited understanding is FM experts at Rockwell contributed to its design even though the implementation itself is unverified. Rockwell engineers are also more expensive than postdocs at NICTA.

[Joe Hendrix]

I mostly wanted to jump into this conversation because I think quoting numbers like this obscures what I think are the main issues with FM adoption. In my opinion, that's mainly a lack of enough existing engineers that understand FM, and a lack of mature tools with good documentation, support, and adoption.

[Kevin Buzzard]

interestingly, that very much mirrors the issues with FM adoption in mathematics departments. Five years ago people like me, Patrick, Heather etc etc (mathematicians working in non-logic areas who knew something about theorem provers) were essentially non-existent, now they are just extremely rare, but things like Lean for the Curious Mathematician mean that there is now a non-zero chance that if you choose a random prestigious maths department there will be one person in there who has actually used a theorem prover once in their life. Still a very long way to go though.

[Zartaj Majeed]

Hi Augusto - I'm also very interested in using some theorem prover framework to model distributed systems applications - I've just started to seriously try out different frameworks - and Lean is the first so far - I feel I'll need to express static mathematical and logic statements as well processes running and communicating in time and space - I have no expectations that I'll be able to do the latter in Lean but I'd like to see what is possible in the state of the art for the former

[Zartaj Majeed]

Joe Hendrix mentioned Ivy above - first I heard of it - it seems to have some great ideas for visualization and testing but the project on github looks pretty stagnant https://github.com/kenmcmil/ivy - has anyone here tried it?

[Chris B]

@Joe Hendrix
Thanks for sharing. I appreciate your perspective with respect to adoption, and it's nice to have an insider's take on how the cost/benefit sausage is made.

[Joe Hendrix]

@Kevin Buzzard Yes, that change in the mathematics community is really exciting to me even if I'm not in a position to contribute. That's one of the messages I learned from your talks that surprised me at the time, but in retrospect seems obvious.

[Augusto Hack]

@Jannis Limperg no discouragement at all, I was really just throwing random numbers around to express my motivation. I also don't really expect to use these tools in practice. The best case scenario is having colleagues saying "cool", but the reality is the vast majority of companies/teams would not accept using these tools in production, specially with another language like lean/gallina, the ecosystem is just not there (virtually impossible to hire people, no libraries, no integration with existing systems, etc.). My interest in the subject is still there though

[Augusto Hack]

@Joe Hendrix cool, recently I also saw Martin Kleppmann advocating for that approach. There is also some movement in the blockchain space to use formal verification, specially for smart contracts, which is also an interesting approach since these usually run on a very simple virtual machine.