Initially I started to take a note here to ask questions here but I ended up with a blog post. I literally copied the text from this slack box to the other one. https://medium.com/@zolipeto/oo-fp-approach-x-formally-locked-in-6ce3c6facd47?sk=481e53e50b018f13ab1110d3fa0139ce I’d really like to see your opinion, have you ever felt like that? What will happen with Formal Proofs in Software? What is your prediction: what/when is the next related, huge thing?

formal proofs can't even prove tic tac toe is correct. They have not advanced to include the concept of something being drawn, or event-driven situations. But any purely computational type of task, like calculating the value of cosine(n), they can guarantee all sorts of good things. So they have made steady progress, but academia doesn't seem to want to move out of the protected grove of pure numerical types of programs. I am not sure if they find it too grubby and boring, or it is just too hard to do. But what product today doesn't draw something or send something across the network? So at the moment languages like Coq and Agda and the other experimental logic languages are so far removed from practicality, that when you talk to these people as i occasionally do, it's like talking to someone from another planet.

Thanks for sharing!