nifty f* -> c

Raoul Duke

unread,

Oct 20, 2016, 1:47:32 PM10/20/16

to ats-lang-users

http://goo.gl/qSf6hF

Kiwamu Okabe

unread,

Oct 22, 2016, 2:49:23 AM10/22/16

to ats-lang-users

On Fri, Oct 21, 2016 at 2:47 AM, Raoul Duke <rao...@gmail.com> wrote:
> http://goo.gl/qSf6hF

Good news for me!

F* is similar to ATS, but F*'s proof function can be called from
dynamic function.
On the one hand, I think F* needs much time to type-check (such like
proof) than ATS language.

I'm afraid that F* can not maintain interaction between the language
and C language better than ATS.
Do you know something around that? > Raoul

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

Kiwamu Okabe

unread,

Oct 22, 2016, 8:24:22 AM10/22/16

to ats-lang-users

On Sat, Oct 22, 2016 at 3:49 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> On Fri, Oct 21, 2016 at 2:47 AM, Raoul Duke <rao...@gmail.com> wrote:
>> http://goo.gl/qSf6hF
>
> Good news for me!

https://github.com/FStarLang/kremlin/blob/master/test/ML16.fst

This example code is very interesting. However, the F* can safely
maintain pointer?

Raoul Duke

unread,

Oct 22, 2016, 10:28:23 AM10/22/16

to ats-lang-users

i do not know.

Reply all

Reply to author

Forward