F*, кодогенерация

Текущая версия — глубокая альфа, и, емнип, F# они генерировать пока не умеют.

Точнее смогу сказать на следующей неделе. Сейчас нет доступа к подходящей для экспериментов машине.

Пишут

The latest version of F* is written entirely in F*, and bootstraps in OCaml and F#

А еще пишут:

https://github.com/FStarLang/FStar/issues/94

The specialization of the ML backend to generate F# is ongoing development and should be available in the near future.

The JavaScript backend (which uses the --codegen JavaScript option contrary to the usage output), it is currently missing some features currently in the ML backend. In particular, it doesn't implement --odir yet.

У меня сейчас под рукой только банка со старенькой виндой, и на ней fstar, поставленный из бинарного пакета https://www.fstar-lang.org/fstar_popl2015.zip, не умеет генерировать ничего, кроме окамла. Ну или я не вкурил что там надо нажать, лол. Мне от эфстара нужен только окамл, так что глубже я особо не копал.

А ты для каких целей собрался его использовать?

Для написания верифицированного ПО под дотнет

не ради холивара, просто интересно, а чем этот ваш F* так хорош, если вкратце?

https://www.fstar-lang.org/

F* is a new higher order, effectful programming language (like ML) designed with program verification in mind. Its type system is based on a core that resembles System Fω (hence the name), but is extended with dependent types, refined monadic effects, refinement types, and higher kinds. Together, these features allow expressing precise and compact specifications for programs, including functional correctness properties. The F* type-checker aims to prove that programs meet their specifications using an automated theorem prover (usually Z3) behind the scenes to discharge proof obligations. Programs written in F* can be translated to OCaml, F#, or JavaScript for execution.

Мануал — https://www.fstar-lang.org/tutorial/
Потыкать можно тут — http://rise4fun.com/FStar

Посмотри тогда и вот это — https://github.com/csgordon/coq-fsharp

Видел и пользовался, просто хотелось посмотреть на сабж. Тем более, что сейчас идет повышение популярности именно general purpose языков с верификацией.

Сейчас очень интересуюсь ATS, потихоньку разбираю код, пишу свои поделки, пытаюсь багрепорты посылать :)

о, спасибо

Можно рассматривать как логическое продолжение F# (c оговорками).

Собрал мастер-бранч с гитхаба. Генерация F# не работает.

alex@debian:~$ mono --version
Mono JIT compiler version 3.2.8 (Debian 3.2.8+dfsg-9)
Copyright (C) 2002-2014 Novell, Inc, Xamarin Inc and Contributors. www.mono-project.com
        TLS:           __thread
        SIGSEGV:       altstack
        Notifications: epoll
        Architecture:  amd64
        Disabled:      none
        Misc:          softdebug 
        LLVM:          supported, not enabled.
        GC:            sgen

alex@debian:~$ cat /etc/debian_version 
8.0

JavaScript:

alex@debian:~/media$ fstar.exe ex1a-safe-read-write.fst --codegen JavaScript      
 (function ()
 {
  var $C = (function (t,v)
  {
   return {
   "t":t,
   "v":v,
   "toString":(function ()
   {
    return this.t + ":" + this.v;
    })
   };
   });
  if(!this.FileName)
   FileName = {};
  
  if(!this.ACLs)
   ACLs = {};
  
  if(!this.System.IO)
   System.IO = {};
  
  if(!this.UntrustedClientCode)
   UntrustedClientCode = {};
  
  })();
Lax type-checked module: Prims
Lax type-checked module: FileName
Lax type-checked module: ACLs
Lax type-checked module: System.IO
Lax type-checked module: UntrustedClientCode

Ну хоть js работает

F* на гитхабе очень активно пилят в последнее время. Подождем-с.

Вот отсюда копипаста:

We now have an F# backend---it’s not 100% functional yet (in particular, the coercions to/from the object type aren’t as fully features as Ocaml’s Obj.magic). But, it is good enough to compile a decent amount of code---we can, e.g., bootstrap now via the extraction to F#. Also, unlike Caml, F#’s type inference is incomplete in various annoying ways (e.g., in how it handles projection) which require many more annotations to be emitted in the generated code than we need for OCaml. So, you may notice some brittleness there.

You can use the F# backend by passing the flag “—codegen FSharp” … you’ll then have to run fsc yourself on the generated .fs files.

I will continue working on it, but if you have code that you want to run in F#, you can give this a go already.

Утянул мастер, собрал, проверяем:

alex@work:~/media/dev/repos/private/FStar/examples/maths$ ../../bin/fstar.exe ../../lib/constr.fst --admit_fsi Set ../../lib/set.fsi ../../lib/heap.fst ../../lib/st.fst ../../lib/all.fst ../../lib/list.fst ../../lib/string.fst --codegen FSharp gcd.fst
extracting: Prims
extracting: Constructive
extracting: Set
extracting: Heap
extracting: ST
extracting: All
extracting: List
extracting: String
extracting: Gcd
Gen Code: Constructive
Gen Code: Heap
Gen Code: ST
Gen Code: All
Gen Code: List
Gen Code: String
Gen Code: Gcd
Verifying module: Prims
Verifying module: Constructive
Verifying module: Set
Verifying module: Heap
Verifying module: ST
Verifying module: All
Verifying module: List
Verifying module: String
Verifying module: Gcd
All verification conditions discharged successfully
alex@work:~/media/dev/repos/private/FStar/examples/maths$ ls -l
итого 52
-rw-rw-r-- 1 alex alex   528 авг.  25 11:11 All.fs
-rw-rw-r-- 1 alex alex   729 авг.  25 10:47 bijection.fst
-rw-rw-r-- 1 alex alex  2834 авг.  25 11:11 Constructive.fs
-rw-rw-r-- 1 alex alex  1116 авг.  25 11:11 Gcd.fs
-rw-rw-r-- 1 alex alex   828 авг.  25 10:47 gcd.fst
-rw-rw-r-- 1 alex alex  1929 авг.  25 11:11 Heap.fs
-rw-rw-r-- 1 alex alex 12450 авг.  25 11:11 List.fs
-rwxrwxr-x 1 alex alex   110 авг.  25 10:47 Makefile
-rw-rw-r-- 1 alex alex   685 авг.  25 11:11 ST.fs
-rw-rw-r-- 1 alex alex  1673 авг.  25 11:11 String.fs

Наконец-то :)