Boole front-end: C0

Stream: CSLib: Code Reasoning

[Chris]

Hello, I'm an undergraduate studying CS and I may be interested in building a Boole front-end in the near future (perhaps in the spring/summer). I was wondering if there are any blockers that might make this impossible / very difficult as of now (and thus I should wait a few months for Boole stability), or if I can begin scoping out this project.

The language I am currently thinking of is C0, a "safer" subset of C developed at Carnegie Mellon, and it's used to teach introductory imperative programming, data structures, and algorithms. I think it's a language which is interesting enough to program interesting things, and could be a worthwhile frontend for Boole. The language also supports program contracts (e.g., preconditions, postconditions, loop invariants/asserts, etc), which makes it have a clean translation for code reasoning in Boole.

The C0 language specs are here: https://c0.cs.cmu.edu/docs/c0-reference.pdf

[Clark Barrett]

Hi Chris - this sounds like a cool project! I wouldn't say there are any blockers, but I expect that each new front end we develop will illuminate weaknesses or missing features in Boole. We do intend to add features to support new front ends, but this may take some time and discussion, so I think that is the main risk you should be aware of.

[Chris]

I see, thank you for the reply!