"Mainstream" programming systems with a Coq-like development style?

Miscellaneous
#1

I rather enjoy the programming style one has to program in when developing in Coq. It’s a fascinating idea: write a specification, then refine it until finished. There’s an addictive, puzzle-like nature to it that i adore. I read on “test-driven development” and i’m like, but the system can help you so much more if you have full specs and not just tests!

Are there any similar systems for more popular languages? That is, would it be possible to use a specification language for something like Python, C, Java, Haskell, etc, and then have some way of using said spec as a guide to writing programs?

PS: Extraction does not count!

(i’m not married to the idea of using tactics; i think what they have working in Agda would be fine, too, in something other than a proof assistant ofc)

1 Like
#2

I guess the B tool is another example of “specify first” style. But then you go by refining instead of programming.

#3

One thing that is important to realize is that “similar systems for more pupular languages” is something very hard to accomplish because the type system of Coq is as complex as you can get. This is not a bad thing, this is the price to pay for expressability.

The reason for Coq using tatics is that building these proofs terms can get arbitrarily complex, so building your programs in a more step-by-step (also called refinement) style is often more convenient. Agda tackles the same problem by providing a better environment to pick into the proof terms in development time, so you rely a lot on your programming environment – usually emacs – to accomplish that.

Now I’m not saying it is impossible to achieve a good specification language that allows you to deal less with proofs, but theorem provers in general are not there yet. I would suggest that you play around with TLA+, Idris and Isabelle to get a taste of other systems with a similar flavor.

Now if you really want to get away from the proofs this is where SMT solvers research shine, the best tool I’ve seen around is SAW toolbench from galois.