search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.68k stars 231 forks source link

Codegen to JavaScript #332

Closed catalin-hritcu closed 4 years ago

catalin-hritcu commented 9 years ago

Reviving the JavaScript backend at some point would be great.

xavierzwirtz commented 9 years ago

When it does come back in, support for AMD modules would be fantastic. As sites grow in scale, supporting dynamic resource loading through AMD becomes a prerequisite. Most transpilations to JS do not support that, which makes them much more painful to use at a large scale.

xavierzwirtz commented 9 years ago

Being able to write a react.js component in F* that could be compiled to an AMD module would make both the lover of strong types, and the front end web dev inside me very happy.

jordwalke commented 8 years ago

@xavierzwirtz: Now that, I'd like to see.

ad-l commented 8 years ago

What is the most popular virtual DOM nowadays? Is jsdom still used?

jordwalke commented 8 years ago

React is probably the most popular "virtual DOM", but it's more than just a "virtual DOM". It's a functional API for composing UIs on top of arbitrary rendering layers including native iOS/Android views (not just the DOM).

alexswan10k commented 8 years ago

Is there any progress on this? I for one am keen to see this working, as in my opinion there are no satisfactory solutions to write ML-derivative code that transpiles to javascript on windows.

I am also a little confused as there are tutorials on this (http://rise4fun.com/FStar/tutorial/jsStar), but the current compiler (0.9.1.1) doesnt seem to accept the "--codegen JavaScript" flag. Is there something I am missing?

On a side note the holy grail for me would be AMD/Systemjs integration, with typescript .d.ts support. One day perhaps :)

catalin-hritcu commented 8 years ago

I am also a little confused as there are tutorials on this (http://rise4fun.com/FStar/tutorial/jsStar), but the current compiler (0.9.1.1) doesnt seem to accept the "--codegen JavaScript" flag. Is there something I am missing?

That tutorial is for an old, different, and unmaintained version of F*. Unfortunately, @nikswamy found no way to remove it from the web, so it keeps confusing people.

alexswan10k commented 8 years ago

Not to worry, thanks for clearing that up.

mk commented 8 years ago

Should it be possible to translate to JavaScript using the OCaml output and either bucklescript or js_of_ocaml?

nikswamy commented 8 years ago

In principle, yes. Although I don't know of anyone who has tried it. If you do, I'd be very interested to learn how it went. Thanks!

catalin-hritcu commented 7 years ago

Marina Polubelova has been working on implementing this last summer on the polubelova_backends branch. Apparently her implementation is quite advanced but it will take some more time until this can be merged back into master. Marina can give more details.

catalin-hritcu commented 7 years ago

More discussion happened on this coq-club mailing list thread: https://lists.gforge.inria.fr/pipermail/fstar-club/2017/000068.html

nikswamy commented 4 years ago

This issue is very old by now.

@cpitclaudel did a lot of work on compiling F using js_of_ocaml, including running F within a browser. That was a couple of years ago, though.

We also have a Wasm backend for KreMLin, thanks to @protz and @denismerigoux

Please reopen this issue if you have anything to add.