epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
359 stars 53 forks source link

Eta/Frege front-end #475

Open romac opened 5 years ago

romac commented 5 years ago

Eta: Blocked by https://twitter.com/rahulmutt/status/1113791731772743680

vkuncak commented 5 years ago

With @redelmann 's new parsing combinator library we should be able to have an alternative Haskhellish front end rather quickly.

romac commented 5 years ago

Yeah I am hoping to be able to implement https://github.com/epfl-lara/stainless/issues/494 and/or merge the WASM backend + add WASI [0] support so that we can have our own little and lightweight language, tailored to the features we support well in Stainless.

[0] https://hacks.mozilla.org/2019/03/standardizing-wasi-a-webassembly-system-interface/

On 17 May 2019, at 17:51, Viktor Kuncak notifications@github.com wrote:

With @redelmann 's new parsing combinator library we should be able to have an alternative Haskhellish front end rather quickly.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

vkuncak commented 5 years ago

Did you see Z3 compiled to WASM?

https://github.com/cpitclaudel/z3.wasm