[nextos]

I completed a MSc in Formal Methods a decade ago, and I've worked in software projects where the level of rigor was equivalent or superior to any classical engineering field. For example, railway signaling or some real time control systems. We handed in complex artifacts that have had zero defects throughout their lifetime (> 15 years).

I believe lightweight formal methods are quite promising and might let software move relatively quickly and economically while retaining some rigor. Look into Liquid Haskell for some ideas that might become mainstream.

[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.

[dmoy]

I personally think it would be excellent if that was the only way you were allowed to code. Though I'd probably lose my job haha. I'd sleep better at night.

[throwmeawayya]

How does liquid haskell compare to typescript?

[CrazyPyroLinux]

Obligatory joke: https://twitter.com/fireship_dev/status/1383835506664906756