[kreelman]

Liquid Haskell looks similar to Eiffel in terms of contracts.

I imagine a whole bunch of power could be derived from this in Haskell. I don't know how heavily contracts were/are used in Eiffel (I don't think it's so popular these days).

It would be great to know if contracts had a measurably useful outcome on projects and what that measurable was (addressed a market that we otherwise wouldn't have been able to, dropped runtime errors to only system based errors, etc).

WRT your projects, I imagine it would be great to see your product out there working with a known level of uptime and quality. I could imagine it's a bit of a shift from the normal "throw it together" of ... a lot of software.

I'd be curious to know what it's like to work on day to day, year to year. I imagine lots of software will still be "throw it together" for a long time yet, but even if the subsystems are formally verified, it could have a useful impact on the software that consumes these (verified) modules.

[nextos]

Liquid Haskell is a bit different from Eiffel. On Eiffel, contracts were designed to be verified at runtime. There were some efforts to verify them at compile time, like Liquid Haskell does, but that's hard unless the whole language and type system are designed for that from the ground up.

As for my day to day job, I think the real difference with common software development was that requirements were very well understood right from the beginning. This allowed us to formalize them into axioms and then derive the implementation in a stepwise fashion using some Standard ML tooling.

I've also worked on proving theorems on existing software artifacts, but that's way harder both in terms of effort and number of defects.