4 ms·
As an undergraduate, I used a research project at my university that did more-or-less what the author describes. The system was an "animator" for formal specif
by ben314 15y ago
As an undergraduate, I used a research project at my university that did more-or-less what the author describes.
The system was an "animator" for formal specifications called Possum:
http://ww2.cs.mu.oz.au/~tmill/tgf/index.html 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?
- jng 15y agoI 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!