COGENT: Certified Compilation for a Functional Systems Language

[Kiwamu Okabe]

Hi all,

I found following paper which explains new language using linear type:

https://arxiv.org/abs/1601.05520

It's a good news for me, because we become to have many choice for
linear type and raw C language.

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Kiwamu Okabe]

On Mon, Sep 19, 2016 at 10:36 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> https://arxiv.org/abs/1601.05520

The code is found at following:

https://github.com/NICTA/cogent

[Kiwamu Okabe]

On Tue, Sep 20, 2016 at 9:24 AM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> https://github.com/NICTA/cogent

However, the cogent is too heavy...

> To build the proofs, it is recommended that your machine (or virtual machine) provides 32G of memory and 4–8 CPU threads.
> Build compilation correctness proof for ext2. (ETA: 120 CPU hours)

I would like to get a light-weight process like ATS, to get more safe
and convenience.

[gmhwxi]

COGENT is a very limited domain-specific language (DSL).

I think what you are doing (c2ats) is the right approach. This is what I
call "meta-programming". But c2ats is still yet too limited...

On Tuesday, September 20, 2016 at 12:14:00 AM UTC-4, Kiwamu Okabe wrote:

[Kiwamu Okabe]

Hi Hongwei

On Fri, Sep 23, 2016 at 12:27 AM, gmhwxi <gmh...@gmail.com> wrote:
> COGENT is a very limited domain-specific language (DSL).

Thanks for your opinion.

> I think what you are doing (c2ats) is the right approach. This is what I
> call "meta-programming". But c2ats is still yet too limited...

Yes. I can't say it's useful for real programming today.
If you have more good idea for c2ats, please send me your issue.

Best regards,

[gmhwxi]

>>If you have more good idea for c2ats, please send me your issue.

I think we need to find a way to translate not only types but also actual
code.

On Thursday, September 22, 2016 at 11:35:34 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei

[Kiwamu Okabe]

On Sat, Sep 24, 2016 at 12:01 AM, gmhwxi <gmh...@gmail.com> wrote:
> I think we need to find a way to translate not only types but also actual
> code.

Do you mean the tool should...

* create accessor for record member?
* translate function body in C language into ATS?

Of course, latter is not easy thing...

[gmhwxi]

I think we need to be able to translate function bodies.

On Friday, September 23, 2016 at 11:13:19 AM UTC-4, Kiwamu Okabe wrote:

[Kiwamu Okabe]

On Sat, Sep 24, 2016 at 6:06 AM, gmhwxi <gmh...@gmail.com> wrote:
> I think we need to be able to translate function bodies.

Umm... I also think it's useful for real programming.
However, do you think it's worth while using following unsafe proof function?

```
extern praxi __create_view {to:view} ():<prf> to
extern praxi __consume_view {from:view} (pf: from):<prf> void
```

For me, it's not trivial that translating C into ATS correctly use
dependent/linear types without such unsafe things... Of course, after
automatically translating, we can modify the generated code into a
style correctly using proof.

[gmhwxi]

The C-to-ATS translation is *not* expected to automatically generate proofs.
The translation is mostly for generating some form of ATS code that can be gradually
improved through manually adding annotation.

On Friday, September 23, 2016 at 7:37:57 PM UTC-4, Kiwamu Okabe wrote:

[Kiwamu Okabe]

Hi Hongwei,

On Sun, Sep 25, 2016 at 5:02 AM, gmhwxi <gmh...@gmail.com> wrote:
> The C-to-ATS translation is *not* expected to automatically generate proofs.

Yes. I agree it.

> The translation is mostly for generating some form of ATS code that can be
> gradually improved through manually adding annotation.

Yes. But the generated code will seem such like following stupid one...

https://github.com/metasepi/c2ats/blob/master/example/gtk3/main.dats#L10

And also, we should think `goto` statement in C language. Real code
has many `goto`s:

https://github.com/IIJ-NetBSD/netbsd-src/blob/5e5e739906b4a97b7b08da1d6cd5eaff1111a1f1/sys/ufs/ffs/ffs_snapshot.c#L1584

How to translate them into ATS code without any exception,
automatically? Some state machine is needed for it?

[Raoul Duke]

i guess there are f.m. tools that claim to prove things about c, although they might not emit proofs in any useful form for other tools.

[Kiwamu Okabe]

Hi Raoul,

On Sun, Oct 2, 2016 at 12:50 AM, Raoul Duke <rao...@gmail.com> wrote:
> i guess there are f.m. tools that claim to prove things about c, although
> they might not emit proofs in any useful form for other tools.

Yes... You are right. I would like to say:

"Such stupid generated code is useful for manually proving?"

And also `goto` statement issue is big problem...

[gmhwxi]

Handling goto's should probably be delayed. At this stage, I think
the focus should be on relatively simple features. For instance, it makes
a lot of sense to just focus on safe use of arrays.

On Saturday, October 1, 2016 at 8:32:22 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

[gmhwxi]

Here is a good example:

https://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html

[Kiwamu Okabe]

Hi Hongwei,

On Sun, Oct 2, 2016 at 12:52 PM, gmhwxi <gmh...@gmail.com> wrote:
> Handling goto's should probably be delayed. At this stage, I think
> the focus should be on relatively simple features. For instance, it makes
> a lot of sense to just focus on safe use of arrays.

Ah, yes. Memory safety is some easy than proving with at-view.

I think I can try this after issue of splitting C headers into treed sats files.

Thanks for your advice,

[Kiwamu Okabe]

On Sun, Oct 2, 2016 at 12:57 PM, gmhwxi <gmh...@gmail.com> wrote:
> Here is a good example:
>
> https://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html

Yes. I already read it.

https://github.com/jats-ug/translate/blob/master/Web/bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.md

I think we can translate C code without `goto` into ATS code, and get
memory safety.