Sorry if this is a naive question. I’m new to the world of proof assistants, and my goal for the year essentially is to become a proficient user, able to write verified software in some domain. Longer term, I really would like to figure out how to make it so that in industry people can write “better” code (more correct, verified, etc).
I’m a deep believer in two things: 1. the state of software is abysmal (look at the 747 max, for example) and 2. we need tools like proof assistants and formal verification to help solve 1. That said, this stuff is not easy. My own background is in data engineering, largely in Java and Scala, and even getting people to use Scala over say Python can be a real battle. People heavily resist the idea of having to “think with a computer” (eg with the compiler), even if ultimately it saves them a lot of time and pain. Interesting Rust has been a bit of a different experience…I don’t know how, but a lot of people I know who would never get excited about Scala or Haskell are excited to write Rust, even though it’s much lower level. This is probably for social reasons rather than technical ones, THOUGH I think that Rust has done a good job, marketing wise, of explaining the problem that the compiler solves for the user.
Regardless…I’m curious what approaches there are to make formally verified more accessible. There are multiple ways to approach this. One is more theoretical: is it even possible? Is it desirable? Perhaps it will always be that a cabal of PhDs will hop from trillion dollar company to trillion dollar company helping them verify critical pieces of infrastructure, while the programming quality tire fire rages on. But the state of security on the web as long as the increasing complexity of software in systems like airplanes and cars makes me hope otherwise.
That said, as I’m new to this stuff myself, it’s sort of hard to imagine where the sweet spot is! Writing Scala or Haskell is easy enough, relatively speaking. Once you have to actually prove things that seem obvious beyond “this function takes these types and outputs this type,” things can get really rough (I’m having flashbacks to the Color module of Software Foundations part 4). I’m currently working through the beta Software Foundations part 5 on Verified C, and I think it’s extremely awesome, but the proofs are not trivial…most critically, figuring out how to represent what is happening in Coq so that a proof is possible is the hardest part, along with coming up with invariants (though I think if you have a good representation the invariants get a lot easier).
So I dunno. I’m wondering if there might be the possibility for domain specific tools (could be a language, but could also be a GUI based something, or anything) that sort of…hide the creation of all of this, but do it under the covers? Where things are correct by construction, and things like representation and invariants are perhaps done by the user, but due to the nature of the constraints of the domain specific whatever, it’s simpler or a good tool can at least make it all more tractable. I have no idea if that is possible or what it would look like, just thinking aloud, and am wondering if there is any work in this direction. I feel like things like Heartbleed and what happened with the 747MAX should be enough to convince industry people that it’s worth the effort but…it seems like that’s not the case, and more effort has to be expended to save software engineers from themselves Or perhaps, to save us from the software engineers!
Edit: I want to add that I’m aware that in the dependently typed language world there are languages like Idris explicitly focused on being something you’d want to write a network driver in. That said, I think the fundamental issue is the same: whether it is Coq or Idris, figuring out how to represent your logic in the system and then verify it is really hard. Idris may have some language constructs to support writing code (whereas most agree Coq excels at writing proofs), but I think the fundamental issue is the same, that the current model of code verification is unlikely to be scalable and we likely will need some other model of doing things if there’s a hope of getting people using these systems. That said, I am also watching the Idris community as I think there’s cool stuff happening there too. But I feel this community has a large, diverse range of practitioners which can lead to cross-pollination of ideas.