moonrocq
A formally verified third-party type checker for MoonBit, extracted from Rocq
type-checker
verified
rocq
coq
moonbit
Author
Version
0.1.0
License
MIT
Repository
Last updated
12 hours ago
Downloads
8
#GreckF/moonrocq
A formally verified third-party type checker for MoonBit.
The checker is written and proved correct in Rocq, and extracted to the
MoonBit code in this module by rocq2mbt. For the supported
fragment of MoonBit it is proved that
- accepted programs are type safe: they never get stuck at run time (they finish with a value of the program's type, or stop in a way MoonBit allows, such as panic);
- checking is decidable: the checker accepts a program exactly when it is well typed.
The Rocq sources, the proofs, the list of supported syntax and the build instructions are in the
GitHub repository. checker/moonrocq.mbt is generated by
extraction; do not edit it by hand.
#Packages
- GreckF/moonrocq/checker: the checker. check_source(src) parses a MoonBit source with the official parser and returns a verdict; render_outcome turns it into readable messages.
- GreckF/moonrocq/cmd/main: a command-line program, moonrocq FILE.mbt....
let (accepted, lines) = @checker.render_outcome(@checker.check_source(src))Command line:
moon build --target native --release
_build/native/release/build/cmd/main/main.exe examples.mbtInstall
Download zipA formally verified third-party type checker for MoonBit, extracted from Rocq
type-checkerverifiedrocqcoqmoonbit
MIT
Updated 12 hours ago
8 downloads