Hi Copilot maintainers,
URML (urml.dev) is a small, Apache-2.0 language for describing robot intent: it validates a request statically against a capability manifest and a safety envelope, then dispatches. The envelope is a declared set of safety properties. Copilot is interesting to URML for the strongest possible version of the runtime half: it generates provably hard-real-time C monitors from stream specifications, the kind used in aerospace.
Nothing here asks Copilot to change or maintain anything. This is a request for comment.
The picture: URML is static and pre-dispatch; a Copilot-generated monitor runs alongside the program as a hard-real-time guard on the same properties. Two real questions. First, can a URML safety-envelope property be expressed as a Copilot stream specification cleanly, and which envelope shapes are awkward? Second, for the hard-real-time guarantee to mean something end to end, what would URML need to declare about its signal sources and timing? I am also reaching Ogma separately, since it generates Copilot monitors from requirements.
Full write-up: https://github.com/URML-MARS/URML/blob/main/docs/rfcs/0364-copilot-rv-outreach.md
Thanks for Copilot; deployable, verifiable runtime monitoring is a real contribution.
Ido Yahalomi (URML, greenvh@gmail.com)
AI-assisted prose, maintainer-reviewed before posting (see VIBE.md). Human-only correspondence available on request.
Hi Copilot maintainers,
URML (urml.dev) is a small, Apache-2.0 language for describing robot intent: it validates a request statically against a capability manifest and a safety envelope, then dispatches. The envelope is a declared set of safety properties. Copilot is interesting to URML for the strongest possible version of the runtime half: it generates provably hard-real-time C monitors from stream specifications, the kind used in aerospace.
Nothing here asks Copilot to change or maintain anything. This is a request for comment.
The picture: URML is static and pre-dispatch; a Copilot-generated monitor runs alongside the program as a hard-real-time guard on the same properties. Two real questions. First, can a URML safety-envelope property be expressed as a Copilot stream specification cleanly, and which envelope shapes are awkward? Second, for the hard-real-time guarantee to mean something end to end, what would URML need to declare about its signal sources and timing? I am also reaching Ogma separately, since it generates Copilot monitors from requirements.
Full write-up: https://github.com/URML-MARS/URML/blob/main/docs/rfcs/0364-copilot-rv-outreach.md
Thanks for Copilot; deployable, verifiable runtime monitoring is a real contribution.
Ido Yahalomi (URML, greenvh@gmail.com)
AI-assisted prose, maintainer-reviewed before posting (see VIBE.md). Human-only correspondence available on request.