search

resource-reasoning / jscert_dev

This repository is now abandoned in favour of using
https://github.com/jscert/jscert
Other
0 stars 0 forks source link

End-user warnings for jsref code without a connected jscert proof #4

Open IgnoredAmbience opened 9 years ago

IgnoredAmbience commented 9 years ago

Coq plugin tooling on targetjs branch may assist with this task. Once proof symbol output is complete, the handler for the ocaml instrumentation could add the proof check? ... No, this is a long way around. Best to explicitly mark as allowable extension in proof and require an alert is produced?