Hi, I have two questions. 1) Are there any plans or discussions on having a subset/extension of C that is designed for formal verification? Much like SPARK wi

Hi, I have two questions. 1) Are there any plans or discussions on having a subset/extension of C that is designed for formal verification? Much like SPARK with ADA. 2) Is there no plan to support GC? Even as an extension of C?