3 ms·

Can someone familiar with this kind of stuff lay out a few benefits of learning this material for a practicing programmer? I'm quite interested (since I've hear

Can someone familiar with this kind of stuff lay out a few benefits of learning this material for a practicing programmer? I'm quite interested (since I've heard a lot about Coq and Pierce) but since there are so many things to learn, I want to prioritize appropriately.

tel 11y ago
It's hard to say exactly. It will teach you to think of programming in an entirely new way. Will that make it easier to write good code elsewhere? Almost certainly if you're not familiar with mathematical proof (maybe you took a discrete math course before). If you know what it is to prove then you'll learn an interesting deep connection between programming and proving. You probably don't want to prove things in your programs. Not really. Even after you learn Coq it's too difficult to do day-to-day. But proofs do not work without being completely consistent in the same way that good programs are. So you can learn a lot of techniques for good programs from techniques for good proofs. Coq rejects bad proofs, so it can be good practice. Finally, Coq is unashamedly higher-order. The chops you gain working with it will translate more or less directly to better functional programming comprehension.
nextos 11y ago
I moved to Scandinavia and got a MSc which was very strong in formal methods: static analysis, model checking and theorem proving; some big names in the field teaching there. I was able to access highly technical programming jobs, those where you are using formal or semi-formal methods to build critical and/or real-time systems. These are very well paid and very nice to work on. You end up designing and implementing very elegant systems with nice guarantees. It feels like high-end engineering. So from a pragmatic point of view, you can access better jobs. From a more idealistic perspective, you will understand computation better.

tel 11y ago

It's hard to say exactly. It will teach you to think of programming in an entirely new way. Will that make it easier to write good code elsewhere? Almost certainly if you're not familiar with mathematical proof (maybe you took a discrete math course before). If you know what it is to prove then you'll learn an interesting deep connection between programming and proving. You probably don't want to prove things in your programs. Not really. Even after you learn Coq it's too difficult to do day-to-day. But proofs do not work without being completely consistent in the same way that good programs are. So you can learn a lot of techniques for good programs from techniques for good proofs. Coq rejects bad proofs, so it can be good practice. Finally, Coq is unashamedly higher-order. The chops you gain working with it will translate more or less directly to better functional programming comprehension.

nextos 11y ago

I moved to Scandinavia and got a MSc which was very strong in formal methods: static analysis, model checking and theorem proving; some big names in the field teaching there. I was able to access highly technical programming jobs, those where you are using formal or semi-formal methods to build critical and/or real-time systems. These are very well paid and very nice to work on. You end up designing and implementing very elegant systems with nice guarantees. It feels like high-end engineering. So from a pragmatic point of view, you can access better jobs. From a more idealistic perspective, you will understand computation better.