H. S. Teoh:
it may be possible in some cases that the compiler can
mechanically
verify a user-supplied proof, and thus provide the same
guarantees
as it would for directly-provable code.
Yes, this is common enough. As an example the Whiley
(http://whiley.org/ ) is not able to find the proof for various
invariants and contracts, but the programmer can write them down
and Whiley verifies them to be correct during the compilation.
Inventing a proof is harder, but verifying it is often much
easier.
The first way D can introduce such things (simple proof) is in
the static verify of some contracts.
Verifying @memoizable or @reflexive/@symmetric/@transitive (for
functions with two arguments) is perhaps a bit too much ambitious
for D compilers. But it surely goes well with the idea of a
language that tries to both avoid bugs and generate efficient
binaries :-) (And perhaps someday C++ Axioms of Concepts will be
handled by a C++ compiler able to verify a function to be
symmetric).
Bye,
bearophile
