Hacker News Reader

Is this about Design by contract? [0] But why do they force students to use an imperative language?

It's not about generating code from contracts, it's about formally verifying that the associated C0 code satisfies those contracts.