Re: [ats-lang-users] Internal error with asserting props

[Hongwei Xi <hw...@cs...>]

>>Actually I have this problem is a more complicated example.
>>I have to write a function returning (as a proof component) something whose
>>(complicated) type has several quantifiers. I first calculate this term in a
>>"let prfn pf [...] in [...]" , then I return it.
>>The problem is probably that I declare the type of 'pf' in the "let prfn pf
>>[...] in", and as the return type of the function, so the type checker has to
>>prove that one is a subtype of the other : problem. But I don't know which
>>type annotation I could suppress, the two seems mandatory...

There are many simple ways to get around this issue. If you put
your code somewhere, I will be happy to take a look.

>>Those "extern prfun" seems to me unnatural.
>>In my opinion, the keyword "extern" is there to tell the typechecker "I'll
>>implement this function elsewhere so trust me, this function will exist."
>>So the "extern prfun" seems to me some "hack", it is accepted by the type
>>checker because the type checker only needs the types, but also by the ATS
>>to C compiler, because proof functions are erased after type checking. This
>>allow writing programs which seems to be proved (are well typed), but which
>>actually depend on unimplemented prfuns, ie potentially wrong assumptions.
>>I noticed that also in listquicksort.dats, there are some unimplemented
>>prfuns, so is this really a totally proved quicksort implementation ?

The problem with providing all the proofs is the heavy cost it incurs;
the programmer spends a lot of time proving things that are "obviously"
true. But I really don't know how to address this issue properly.

>>I solved the first two Project Euler's problems (http://projecteuler.net) in
>>ATS (I don't have a website yet but I'm working on it, for the moment you
>>can find the code for the first problem at "
>>http://www.eleves.ens.fr/home/brunerie/p1_dats.html", and the like for the
>>problem 2). I'm working on the problem 3 but it is much more difficult than
>>the first two.

I took a look. Pretty nice!

>>I tried to write the code in three parts :
>>1) write a prop encoding the problem
>>2) write the type of the function pn which must solve the problem, and
>>implement the function "main"
>>3) implement the function pn
>>
>>I would like that, after reading only the first two parts, the reader could
>>be certain that if the code compiles, then the program terminates and gives
>>the correct result, whatever is written in the third part; the idea being
>>that the proved implementation can be very complicated but if ATS/Anairiats
>>accepts it and if the type is correct, then the program should be correct.

That is what I thought as well when I started the ATS project. But this
approach seems too costly when applied to large and realistic problems.

>>The idea to declare the PRIME prop abstract and to write prfun for the
>>needed properties looks interesting, but that means that I should write
>>extern prfuns only in the first part (the "human verified part") but not in
>>the third (the "machine verified part") because there this would be
>>cheating. In this context, I'm not sure this would be a satisfactory
>>solution.
>>
>>"extern prfun" is useful sometimes, I use it for example in the problem 3
>>for debugging, to check that some parts of the program are correct without
>>having to prove anything at once, but I consider that a problem is solved
>>only if there is no more "extern" in the code.

We could require that all the extern proof functions in a program be  
implemented before the program can run. I may add a flag to control this.

>>Perhaps I have not the good point of view, or at least not the same as
>>yours.

We all have different views :) My view was similar to yours, but it has
since changed.

Cheers,

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hw...@cs...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)