Hoare statements with inline code and abstract statement extensions #958
Description
Opening this thread to discuss the design and implementation of inline code in hoare statements and the extensions to the integration of abstract statements.
The goal is to be able to modularize proofs by allowing better reasoning on programs where part of the code is abstract.
The initial idea is to axiomatize the abstract code via hoare statements which are given as assumptions in the proofs and which then have to be discharged with the concrete code of the program used to instantiate the general statement.
This should allow for less code duplication and more succint proofs.
This would also imply some refactoring of the stdlib to use this more modular approach, and this refactor can serve as a guiding example for the development.