Metasepi's year 2015

[gmhwxi]

It is an interesting read:

http://www.metasepi.org/en/posts/2015-12-31-yuku-kuru.html

Cheers!

--Hongwei

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Jan 2, 2016 at 1:45 PM, gmhwxi <gmh...@gmail.com> wrote:
> It is a interesting read:
>
> http://www.metasepi.org/en/posts/2015-12-31-yuku-kuru.html

I have a question. What is large difference between ATS's proof and VeriFast?
I found the VeriFast on your paper. It's very interesting.

http://people.cs.kuleuven.be/~bart.jacobs/verifast/

Thanks,
--
Kiwamu Okabe at METASEPI DESIGN

[Hongwei Xi]

I have never really used VeriFast in depth.

I have been trying to advocate program-first program verification for

quite some time.

By the phrase 'program-first', I mean that the first priority of program verification

is to facilitate the construction of programs. In Spark Ada, people talk about CbC:

Correct-by-Construction.

My impression of VeriFast is that it primarily focuses on verification by annotating

C/Java code. Clearly, we must ask: How is the C/Java code obtained in the first place?

ATS focuses more on program construction, and program verification in ATS is just part
of program construction. For instance, features like abstract types and templates in ATS
are designed primarily to facilitate program construction.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmnH0x3UD1XJ_Gy5TxCdj-qBYdkftMRFbiX9QWhZdLz%3Dw%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei,

On Sat, Jan 2, 2016 at 2:39 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> I have never really used VeriFast in depth.

O.K. I'll try to use the VeriFast in my work. It will show some results.

> ATS focuses more on program construction, and program verification in ATS is
> just part
> of program construction. For instance, features like abstract types and
> templates in ATS
> are designed primarily to facilitate program construction.

I agree. VeriFast uses C language as the host language, then it can't
use rich type such like abstype or datatype.

How about difference between applying Prop to function and
pre/post-condition as comment in function?
The former is ATS style. The latter is VeriFast style.

[gmhwxi]

Using proofs (that is, programming with theorem-proving) allows the programmer
to have much tighter control over the constraint generation during typechecking.

You can also use pre/post-conditions in ATS:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3

If it worked, I would have really wanted to use it. At present, I find it nearly impossible
to figure out the cause of an unsolvable constraint.

[Kiwamu Okabe]

On Sat, Jan 2, 2016 at 3:10 PM, gmhwxi <gmh...@gmail.com> wrote:
> You can also use pre/post-conditions in ATS:
>
> https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3

Umm... I should learn patsolve this year.