RUGE [1] is another open source PROLOG framework for functional and load testing. Brendon McCarthy originally developed it for testing financial applications at American Express.
Brendon presented it at the 2013 Workshop on Domain-Specific Languages for Financial Systems [2]. One observation made by the Haskellers was that PROLOG approaches such as these are attempting to solve a problem that has already been solved by QuickCheck [3].
There's two different issues here: (1) whether or not to use compiler plug-ins, and (2) whether or not to use compiler plug-ins for metaprogramming.
Using plug-ins for automated analysis improves the quality of your codebase. The annotations serve as a machine-checked documentation which make the code easier to debug.
As you point out though, the benefits of plug-ins for metaprogramming (such as implementing a DSL) is not always as clear-cut: you have to pay the price of maintenance, much of which is not always obvious up-front.
You face many of the same issues when designing a DSL in Scala --- the DSL may generate code that depends on a custom run-time or library.
Java 8 adds support for type annotations, which enables developers to write code such as:
@Currency("USD") double amount;
These annotations can be checked automatically using a compiler plug-in, such as the Checker Framework [1]. The Checker Framework comes pre-packaged with a units checker [2] along with checkers for null pointer errors, locks, string formatting, security, and many more.
Java's domain-specific language (DSL) features aren't as rich as Scala's. However, you could implement some DSL-like features using aspect-oriented programming (AOP) tools or other similar compiler plug-ins.
It depends on whether or not the buyer allows for proof irrelevance.
There are cases where _human_ buyers care about the structure of the proof. In particular, just like with code, you'd prefer a proof that is maintainable, modular, and not-too-hard to update if your assumptions or claim changes.
You'd run into a problem if you let workers introduce assumptions (since introducing a contradiction lets the worker prove anything).
With Coq, you don't have a problem of unsoundness. The problem you have is that the difficulty / time it takes to write a proof is often very sensitive to how you've written your assumptions and formulated the claim. You'd likely want to add a mechanism to the marketplace to reward workers for suggesting ways to improve the problem formulation.
For my Java project, we were using ESC/Java2 under the hood which is unsound in a lot of ways. We definitely observed workers taking advantage of these (either intentionally or not).
One limitation of these crowd-sourcing approaches is that, in practice, validation ("are we trying to build/prove the right thing?") is as important, if not more important, than verification.
[1] this might not be quite true yet, since a solution of "admitted." would pass the Coq checker.
What application domain are you working in that you know all the currencies at compile-time?