[smj-edison]

I'm curious to see if formally verified software will get more popular. I'm somewhat doubtful, since getting programmers to learn formally math is hard (rightfully so, but still sad). But, if LLMs could take over the drudgery of writing proofs in a lot of the cases, there might be something there.

[gjadi]

How is getting proof one doesn't understand going to help build safer system?

I want to believe formal methods can help, not because one doesn't have to think about it, but because the time freed from writing code can be spent on thinking on systems, architecture and proofs.

[smj-edison]

That's a fair question, and looking at my post I now realize I have two independent points:

1. A proof mindset is really hard to learn.

2. Writing theorem definitions can be hard, but writing a proof can be even harder. So, if you could write just the definitions, and let an LLM handle all the tactics and steps, you could use more advanced techniques than just a SAT solver.

So I guess LLMs only marginally help with (1), but they could potentially be a big help for (2), especially with more tedious steps. It would also allow one to use first order logic, and not just propositional logic (or dependant types if you're into that).

[stringfood]

I am so exhausted with being asked to learn difficult and frankly confusing topics - the fact that it is so hard and so humbling to learn these topics is exactly why everyone is so happy to let AI think about formal programming and I can focus on getting Jersey Shore season 2 loaded into my Plex server. It's the one where Pauly D breaks up with Shelli