I've looked into Coq and like a lot of others here tried to learn the theory and application but it is so far removed from my daily work that the benefits are basically non-existent. I've gotten way more mileage out of trying to learn systems theory and cybernetics than anything related to dependent types.
People think this is a tool problem but it's not. Well, the tools kinda suck but fundamentally it comes down to culture and mind share. My background is in pure math but my programming knowledge is steeped in the hacker tradition. It is very hard to overcome all that momentum.
There is no killer application for verified programming. Whatever you can do in Coq in 10 weeks you can do in C in 2 weeks with a few extra buffer overflows. We'd be further ahead if there were more tools for validating C code than trying to rewrite the world with dependent types.
You're right it does come down to culture and mind share. That's why the author already admits this would be a long process. But I think he's right and to truly call what we're doing software _engineering_ there needs to be a more formal basis for how to do things and especially to discern between this is right and this is wrong.
No offense to you, but often times people that entered programming originally from related fields and taught it themselves give me the hardest time working with them. Like, no it's not enough that the software now provides this feature but you copied 1.200 lines of code for it and just squeezed in your if-branches and for-loops somewhere. Your job as software developer is to think how you can wed these new requirements with our existing codebase for others to build upon.
Sorry, but as a bit of a pedantic and clean code enthusiast this is kind of a passion topic for me :)
People think this is a tool problem but it's not. Well, the tools kinda suck but fundamentally it comes down to culture and mind share. My background is in pure math but my programming knowledge is steeped in the hacker tradition. It is very hard to overcome all that momentum.
There is no killer application for verified programming. Whatever you can do in Coq in 10 weeks you can do in C in 2 weeks with a few extra buffer overflows. We'd be further ahead if there were more tools for validating C code than trying to rewrite the world with dependent types.