I've always wondered this - Does the compiler actually use all that contract inf... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		OnlyOneCannolo on Aug 23, 2020 \| parent \| context \| favorite \| on: Bare Metal Rust Generics I've always wondered this - Does the compiler actually use all that contract information, or is it just the prover?

shakna on Aug 23, 2020 [–]

As of Ada 2012, the redesign means that the compiler can make use of the contract information, and was one of the main reasons for a lot of the changes.

OnlyOneCannolo on Aug 24, 2020 | [–]

That makes sense. Otherwise why bother conflating the programing language with the verification language.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact