2 ms·

I wonder why they have not used Coq's extraction approach?

• gsps 9y ago
  As far as I understand, their approach is exactly that, i.e., another target language for extraction. Synthesis is a bit of an overloaded term.
  • unboxed_type 9y ago
    "The compiler itself is also written in Scala and its underlying Coq parser is largely based on the use of parser combinators" while "true" extractor has to be written in Coq, as I understand :-)
    • nickpsecurity 9y ago
      When I read that, I thought "What a huge TCB versus what's typical." Additionally, there exist verified strategies for parsing that might be applicable to Scala. Depends on if their formalisms can handle the language's grammar or whatever. Additionally, if they write untrusted parts in ML, they can supplant it with stuff like property-based testing or CakeML compiler.