rhombus-prototype icon indicating copy to clipboard operation
rhombus-prototype copied to clipboard

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

Open jeapostrophe opened this issue 6 years ago • 2 comments

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.

jeapostrophe avatar Jul 14 '19 16:07 jeapostrophe

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

samdphillips avatar Jul 22 '19 16:07 samdphillips

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.

jeapostrophe avatar Jul 22 '19 16:07 jeapostrophe

Categorizing as "yep moving on" on the grounds that annotations fit this idea.

mflatt avatar Mar 14 '25 19:03 mflatt