Make an RFC for embedding types, contracts, and other specifications

[jeapostrophe]

A key idea, for me, is to be able to separate specifications from the code that uses them, so multiple modules can use the same specification. Here specification is types, contracts, tests, theorems that are true about the software, and so on.

[samdphillips]

Can you see this as a mechanism to compile code without contracts?

[jeapostrophe]

Yup. My perspective is that we should write down very expressive specifications (theorems and contracts with lots of dependencies and precision) and be able to smoothly compile them in a variety of policies from full enforcement and testing to no-seatbelts-or-helmets.