magmide VS practical-fm

https://github.com/magmide/magmide when

How close are we to this https://github.com/magmide/magmide

IME Lean and Coq/Rocq are used more in practice, and have bigger libraries and communities, than Idris and Agda.

Rocq is the most common for program verification, but I suspect mainly due to it being older, and it has weird quirks due to its age, so Lean may catch up. Lean is the most common for proving mathematical theorems.

Big projects verified in Rocq include CompCert, CertiCoq, and sel4. Additionally, some large companies use Rocq to verify critical software like in airplanes (there's a list at https://github.com/ligurio/practical-fm although it may not be accurate). Big projects in Lean include mathlib (collection of various mathematical proofs) and the ongoing work to prove Fermat's Last Theorem. Terrace Tao uses Lean. I'm not aware of "real-world" projects in Idris and Agda but may be wrong.

That said, they're all small communities compared to something like C++ or JavaScript. Moreover, verifying programs is very slow and tedious (relative to writing them), so I wouldn't be surprised if we see a big breakthrough (perhaps with AI) that fundamentally changes the landscape. But remember that even with a breakthrough your skills may be transferable.

https://github.com/ligurio/practical-fm Look for Coq, Agda, Idris, MS - F*.

Does your current company have FM positions? Maybe you could work and learn at the same time. There are a lot of big name companies that are really investing in FM now that more tools are available. Here’s a list someone compiled that can give you an idea of where it’s being used in industry. I see some info is not quite up-to-date (e.g., IBM does have FM, or formal verification, in the US but I think most research is out of their Israel lab; Rockwell Collins is now Collins Aerospace after being acquired by UTC Aerospace).

When you say "formal verification methods", what kind of techniques are you interested in? While using interactive theorem provers will most likely not become very widespread, there are plenty of tools that use formal techniques to give more correctness guarantees. These tools might give some guarantees, but do not guarantee complete functional correctness. WireGuard (VPN tunnel) is I think a very interesting application where they verified the protocol. There are also some tools in use, e.g. Mythril and CrossHair, that focus on detecting bugs using symbolic execution. There's also INFER from Facebook/Meta which tries to verify memory safety automatically. The following GitHub repo might also interest you, it lists some companies that use formal methods: practical-fm