Metasepi's year 2015

Google Group
1

It is an interesting read:

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

Cheers!

–Hongwei

2

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.On Saturday, January 2, 2016 at 12:53:02 AM UTC-5, Kiwamu Okabe wrote:

Hi Hongwei,

On Sat, Jan 2, 2016 at 2:39 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> 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.

Thanks,

Kiwamu Okabe at METASEPI DESIGN

3

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.On Sat, Jan 2, 2016 at 12:16 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi Hongwei,

On Sat, Jan 2, 2016 at 1:45 PM, gmhwxi gmh...@gmail.com wrote:

It is a interesting read:

Metasepi's going year and coming year, 2015 - Metasepi

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.

Papers on VeriFast

Thanks,

Kiwamu Okabe at METASEPI DESIGN

–
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
.