search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
438 stars 63 forks source link

Create "certified term" type #49

Open atomb opened 9 years ago

atomb commented 9 years ago

Currently, it's possible to construct SharedTerm objects in SAWScript that are not well-typed. They can be checked after the fact, but this can be expensive for large terms. Better would be to have an abstract type for terms that are guaranteed to be well-typed, along with functions to combine them with the minimum additional checking to ensure that the result is well-typed.

atomb commented 9 years ago

This should be a saw-core ticket. Closing and re-opening there.

brianhuffman commented 2 years ago

This was originally re-opened as GaloisInc/saw-core#18, which was accidentally closed when the saw-core-coq repo was merged into saw-core (by a commit that had closed saw-core-coq issue 18).

Anyway, this issue has never been addressed, and we need this feature as much as ever. Building ill-typed saw-core terms is still very much a problem, and having a certified term type would help us avoid such situations, or at least to detect them much earlier.

See the comments on GaloisInc/saw-core#18 for some ideas about how such a feature could be implemented.