I agree that’s cause for celebration; even if it is only one line removed (actually I noticed another prval line is dropped too, if trivial), I feel more than half the battle with ATS for me, now, is recognizing when a constraint issue arises because the solver cannot solve the constraint because either 1) it is not possible in the solver or 2) it is not possible mathematically. The former could be thought of as a “soft programmer error” and the latter is a “hard programmer error”, or traditional error in programming logic. So anything that reduces the occurrence of 1) is nice.
There are several issues. What happens if the solver assert returns “unknown”?
It would seem sane to (a) issue a warning and (b) assume the assertion
is correct anyhow.
The second issue arises from this: if the assertion (a) returns unknown or
(b) the programmer suspects it might return unknown, how can the
programmer give the solver some help?
I believe it is sane in a PL that the solver can be:
(a) dropped altogether whilst debugging and developing
(b) activated during a verification pass
(c) the results should be cached to speed up verification
(d) the solver can be swapped for another solver
When I tried to something similar in Felix I divided assertions into
several categories:
1. Axioms. The basic rules (though not necessarily independent)
2. Lemmas. Simple rules an automatic theorem prover could solve
3. Theorems. Rules that would be too hard for an automatic solver
but which might be proven by a proof assistant if hints
were given (in some as yet unspecified language)
I also provide reductions, which are “directed” axioms, that is,
instructions to the compiler to replace some term with another
(hopefully more efficient one).
In principle there is another option. If an assertion cannot be verified
at compile time, generate a run time check.
I think ATS has now run into the problem that some basic assertions
can always be checked efficiently, however once one starts providing
more advanced capabilities, the performance of the verification
system becomes an issue.
One must recognise that dynamically typed scripting languages
(include crap like Java) are popular because they reduce notational
demands, compile fast, and run at quite reasonable speeds for
many purposes (especially with JITs). What’s more, they permit
very high level expression which most statically typed systems do not.
For example few static languages have a type system strong enough
to do functorial polymorphism, not even Haskell can do that.
C++ can do a bit of it, partly because the type system is weaker.
Given this, a practical statically typed language … and ATS is intended
to be a production language not an academic toy … has to be able
to achieve some kind of balance for which the extra cost is worthwhile.
In Ocaml, for example, type inference relieves some of the notational
overhead (at the cost of sometimes incomprehensible error messages).
I will relate a story. I was working at a place on software to verify
C and C++ programs. This was done by constructing a flow model
(control and data) and examining paths: standard static analysis
stuff. However the novel feature of the system was to use a satsolver
to find potential bugs. The satsolver was very fast. However, it wasn’t
accurate because the analysis was only first order. To check for
null pointer issues, one needs a full data flow analysis which is O(N^3).
[The solver was basically O(N)]
So how could the product be improved without killing performance?
The very smart suggestion was made: use the satsolve to find
potential problem areas and apply the full data flow analysis to
just those areas.
Here’s another story. Clang has static analysis and does optimisations.
However some of the optimisations, despite assertions to the contrary
from the developers, are not linear. Most advanced optimisations can’t
be linear. So I suggested a simple solution: do the advanced optimisations
under a timer. Just give up if it is taking too long. increase the time period
for better results. That was pooh poohed by the developers because
the output wouldn’t be deterministic, but they clearly didn’t understand
that the tradeoff between compiler performance and the resulting
program performance is fairly indeterminate anyhow: high level
optimisations are highly sensitive to context, and only work as
expected a small fraction of the time, because one simply cannot
reapply them in every possible context they might be applied.
The bottom line is to do anything advanced you HAVE to develop
some nasty heuristics to keep the compile time/run time tradeoff
reasonable. It’s similar to say a garbage collector. The theory is
all very well but the key to a good GC is the tuning parameters.
What I suspect ATS is going to have to do is provide, along with
the proof data, estimates of the costs of finding a solution.
One then uses linear programming to choose which things
to prove and which ones to give up on. TeX uses this to calculate
line breaks in a paragraph efficiently (one provides a “badness”
rating for various possible line breaks and the solver tries
to minimise the overall badness).
In other words, you need a linear model to cost operations
so as to decide when to apply non-linear operations 
john skaller
ska...@users.sourceforge.net
http://felix-lang.org