Possum would allow you to directly execute a program that was formally defined using the Sum formal specification language. While it was not able to handle every possibility, I found using it to be a really magical experience.
However, in practical terms, the idea of declarative programming has just as many difficulties as ordinary programming: how do you know your specification is correct? how do you debug a logical expression? how do you know your specification matches what you want it to do?
I will look at the project, sounds interesting. If it's like that, I can only
I know declarative doesn't solve the problem of correctness. It's really difficult to define correctness per se! But what such an approach really gains is that you can forget about off-by-one errors, unforeseen cross-conditions in stupid details, so much repetitive code, etc... you will still have the higher-level problems of programming, the efficiency problems, the spec-correctness problems, etc... but nowadays you have those, plus the nitty-gritty details of programming in our paleolitic languages!
I know there are a few initiatives in this area, I really want to have an everyday tool that allows using that kind of approach for everyday problems. It will just make everything so much better for us programmers!
The system was an "animator" for formal specifications called Possum: http://ww2.cs.mu.oz.au/~tmill/tgf/index.html
Possum would allow you to directly execute a program that was formally defined using the Sum formal specification language. While it was not able to handle every possibility, I found using it to be a really magical experience.
However, in practical terms, the idea of declarative programming has just as many difficulties as ordinary programming: how do you know your specification is correct? how do you debug a logical expression? how do you know your specification matches what you want it to do?