Hacker News Reader

Comment by thesuperbigfrog | Hacker News Reader

>> A serious take on a contract-based language

Ada has design-by-contract as part of the language:

https://learn.adacore.com/courses/intro-to-ada/chapters/cont...

Since Ada is used for safety-critical systems programming you could argue that it is very serious about it.

>> And tool integration! One of the coolest things Eiffel sorta did was use contracts to infer tests. If you have contracts, you can use a fuzzer to get integration tests for free.

How about tools that extend design-by-contract to formal verification?

https://learn.adacore.com/courses/intro-to-spark/chapters/01...

SPARK is limited to a subset of Ada, so it is not without limitations, but it can be very useful depending on what you are trying to do.

View on HN

If Adacore had published a full featured free compiler for students/universities by the time Ada 95 standard was published, I am sure that Ada could have occupied the space C++ takes today.

Mostly what Ada lacks is not the features but the comunity effect, we saw that when comparing feature parity with C++ and we see that again when comparing feature parity with Rust.

There are a lot of briliant features and tooling in Ada, but unless there is a community effect (or a gigantic industry sponsor e.g. golang) it is difficult to convince people to switch over.

I can't remember who said it so I will paraphrase, the best language/target to program in is whatever your friends/colleagues are using.

>> If Adacore had published a full featured free compiler for students/universities by the time Ada 95 standard was published, I am sure that Ada could have occupied the space C++ takes today.

Agreed. If there had been more free (gratis) or low-cost Ada compilers at that time Ada would be far less niche than it is today.

There is increased interest in Ada today thanks to Rust. There is also interplay between Rust and Ada/SPARK features with Rust getting some Ada features and SPARK getting some Rust features.

Ferrous Systems is working with AdaCore on the Ferrocene Language Specification to formally document the Rust subset that Ferrocene will use:

https://ferrous-systems.com/ferrocene/

https://ferrous-systems.com/blog/ferrocene-language-specific...

It is exciting to see Rust mature so it can one day be used in safety-critical work.

This seems to be a common theme among certain languages, software, etc. from the 90s. I've heard similar things about Smalltalk.

Long before the digital era that common theme would have been expressed as —

Don't look a gift horse in the mouth.

Yup, also the commercial ADA IDEs were brilliant, even compared to Borland, but o-so-expensive.

> If Adacore had published a full featured free compiler for students/universities by the time Ada 95 standard was published, I am sure that Ada could have occupied the space C++ takes today.

The same can be said about Eiffel.

Or Delphi

> If Adacore had published a full featured free compiler for students/universities by the time Ada 95...

Didn't they? I wasn't around then, so I'm working with what information I can find online. According to Wikipedia it was fully validated in 1995[1], and I'm pretty sure it was always a free compiler based on GCC. I think the dust had settled on the battlefield of the language wars long before Ada 95. It was/is still common for European universities to teach Ada as part of the computer science curriculum. That still hasn't managed to give Ada the industry presence it deserves. In my opinion it's by far the superior language. It's just losing out for human reasons.

> ...gigantic industry sponsor e.g. golang...

It had the biggest industry sponsor at one stage: The US Department of Defense. Back in the late 70s, and early 80s when the DoD was directly sponsoring Ada's development, they had incredibly deep pockets. I'd say this is why Ada is so comprehensive today. They had the money, and motivation to design the language by committee down to the most minor details.

[1] https://en.wikipedia.org/wiki/GNAT

Ada 83 had long had a reputation for stunningly high prices when my first job chose C++ in 1992 (when templates were pretty new and sort-of worked).

I guess that prior to the FSF releasing GNAT, and the DoD dropping its Ada mandate, compiler vendors had a captive audience, and could charge a serious premium for their software.

I've read that the hardware required to use an Ada compiler was far more expensive than its competitors as well. I've heard more than one person say that this was a serious barrier to its adoption in the wider industry.

The D programming language, too.

https://dlang.org/spec/function#contracts

+1 on D. It even has contracts for members.

Forgetting about SPARK was a big whoops for me.

(Lots of formal verification languages are based on contracts, like SPARK, Frama-C, and Dafny. I'm interested in uses for contracts that aren't just formal verification, though!)

>> I'm interested in uses for contracts that aren't just formal verification, though!

Ada 2012 design-by-contract features aren't just for formal verification, they can be used in a general purpose way similar to Eiffel:

https://learn.adacore.com/courses/intro-to-ada/chapters/cont...

Can you elaborate a bit more about the wanted features for a language with semantic relations?

An example off the top of my head would be writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test. Another idea would be being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other. I don't know how useful this would be in practice, but it seems interesting to me!

>> writing a serializer/deserializer pair and explicitly saying they are inverses of each other, as opposed to having to implicitly say that in a round-trip property test.

That capability would be very useful. There are many cases where I have had to define serialization and deserialization functions for numerous objects and had to create so much "boilerplate" unit test code like you describe. It made me wish I was using a Lisp with built-in reader and printer functions.

>> being able to say that two data representations are isomorphic under a given transformation, so I can define a function for one transformation and call it on the other.

This strikes me as very Haskell-ish, but could be quite useful to ensure certain properties or invariants.

I use fuzzing for this. In fact that's the main case I use it for.

Better still would be to take progressively typed languages, combined with contracts and property-based testing, and iterate toward a more precise contract for all of your code whenever it became necessary or whenever you got bored.

What are the consequences of deciding that no Foo's are allowed to be red? Hmm, that's interesting/unintended...

The main difficulties with statically typed languages seem to be both 1) quickly arriving at a workable prototype, and 2) dealing with the consequences of regrettable decisions made early on. Those two being in tension contributes a lot of drama, and not just in analysis paralysis.

Also Nim has contracts and supports formal proofing: https://nim-lang.org/docs/drnim.html

A more practical one might be this contracts library https://github.com/Udiknedormin/NimContracts

Its not public language, but at Risk Management Systems, I worked on Contract Definition Language- an external DSL for computable insurance, re-insurance contracts. This was used to simulate insurance losses when catastrophic events happen (earthquake, hurricane)

Any good reference for that CDL? The idea seems quite useful for what I'm working on. All I found is a wishy-washy doc with poorly chosen examples [0]

[0] https://www.riskdataos.org/html/HelpCenter/Content/CDL/CDL_S...

RMS never played nice on interoperability. I wouldn’t bet on the CDL to become a useful standard, because it is under-powered, under-specified and stagnant.

The “open” alternative is OASIS. Their Open Exposure Data standard [1] is complete and supported by many industry participants. Unfortunately it’s a database based format, rather than a text based DSL, but still betterthan the alternatives.

[1] https://github.com/OasisLMF/OpenDataStandards/tree/master/Op...

Thank you! I wasn't aware of OASIS. Reading up now.

When I read "contract-based language"I immediately thought of Ada. I could be wrong but I think SPARK is incorporated into the Ada 2022 standard at this point, it could really be thought of as part of the language.

It's the furthest thing from a "dynamically typed language" but it can probably also check the "math" requirement here too.

Fuzion has contracts as well:

https://flang.dev/tutorial/pre_post_conditions https://github.com/tokiwa-software/fuzion

Disclaimer, I work in the Fuzion team.

Java has a similar “extension” as well: https://en.m.wikipedia.org/wiki/Java_Modeling_Language

Similarly, Ruby had RDL - which implemented pre/post contracts and type checking prior to Sorbet. It was actually pretty nice, if slow.

https://github.com/tupl-tufts/rdl

Reply on news.ycombinator.com