D enters Tiobe top 20

Walter Bright newshound2 at digitalmars.com
Tue Nov 12 09:12:13 UTC 2019


On 11/11/2019 8:25 PM, Doc Andrew wrote:
> I think _most_ people consider Assert vs Assume the way SPARK and F* do - as 
> seen here: 
> https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-between-assert-and-assume/ 

Which says:

"Intuitively, Assert is something that you expect the static checker be able to 
prove at compile time, whereas Assume is something that the static checker can 
rely upon, but it will not try to prove. At runtime Assert and Assume behave the 
same: If the condition is false, then the program fails – how it fails (e.g., 
throwing an exception, opening a dialog box, etc. can be completely customized 
with CodeContracts)."

Therefore after the Assert, the prover can assume the Assert condition is true. 
If the prover can prove the Assert is always true, the runtime check can be 
safely removed.


More information about the Digitalmars-d mailing list