Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Ada's dependent types, and its types as a whole

nytpu.com

Post reply on HN
Print view View original

21–30 of 146 posts

Re: Ada's dependent types, and its types as a whole

#21

Post by quietbritishjim »

LiamPowell wrote: post #7
seabird wrote: post #6

Ada is a criminally underrated tool that is unfortunately probably doomed to perpetually take the backseat to Rust despite Rust not solving all the problems Ada does. It's really sad that so many people's idea of safe programming is pretty strictly limited to memory safety, and that because Ada's baseline memory safety (SPARK is a different story) isn't as robust as Rust's borrow checker (in the sense that it doesn't…

I'm a bit disappointed that we've ended up with Rust in the kernel but not Ada. The kernel relies on GCC and there's already an Ada compiler in GCC, so it wouldn't require adding another compiler as a build requirement like Rust does. There's a couple of major advantages that Ada could have in the Linux over Rust for safe drivers: 1. Having the option to use SPARK for fully verified code provides a superset of the co…

> 2. Representation clauses almost entirely eliminate the need for the error-prone manual (de-)serialisation that's littered all over Linux driver code:

Do representation clauses let you specify endianess? From a quick glance at that link it didn't appear so. I would imagine that invalidates most use cases for them.

Re: Ada's dependent types, and its types as a whole

#22

Post by jonlong »

chamomeal wrote: post #18
jonlong wrote: post #15

Coming from the type theory side with only a passing glance at Ada, I am nevertheless sure: this is not what type theorists mean when they talk about dependently typed languages. Such languages derive from the formulation of Per Martin-Löf (also called Intuitionistic Type Theory), they include dependent sum and dependent product types, and they allow type checkers to prove complex statements about code. (The history…

Super interesting! Thanks for the link. Would you say Lean is a somewhat learnable language for somebody who only has cursory exposure to functional programming and static types? I’ve almost exclusively used typescript for the last few years, except for some clojure in the last few months. Sometimes I find a neat language, but my very TS-oriented brain has a hard time getting into it.

I would say dependent types are going into the deep end; unless you have a real need to prove things, it may be hard to see the motivation to learn such abstractions.

In between ad hoc types like TypeScript and dependently-typed languages like Agda, Coq/Rocq, and Lean are well-typed, polymorphic (but not dependent) languages like OCaml, F#, or Haskell ("ML family" or "Hindley-Milner" are related terms). Those are what I'd suggest checking out first!

Re: Ada's dependent types, and its types as a whole

#23

Post by rtpg »

LiamPowell wrote: post #20
jonlong wrote: post #15

Coming from the type theory side with only a passing glance at Ada, I am nevertheless sure: this is not what type theorists mean when they talk about dependently typed languages. Such languages derive from the formulation of Per Martin-Löf (also called Intuitionistic Type Theory), they include dependent sum and dependent product types, and they allow type checkers to prove complex statements about code. (The history…

> An example of something you can do in a dependently typed language is write a sorting function in such a way that the type checker proves that the output will always be in sorted order. I am pretty sure this cannot be done in Ada; checking at runtime does not count! It actually can be done in Ada, but not purely with the type system, instead we rely on SPARK, which converts Ada code and passes it through various au…

what is the flow for working through this kind of proof? Is there an interactive proof mode like you find in a lot of dependent type provers? Or is there some other guiding mechanism for telling you that you haven't provided enough guidance with asserts?

Re: Ada's dependent types, and its types as a whole

#24

Post by LiamPowell »

quietbritishjim wrote: post #21
LiamPowell wrote: post #7

Earlier quoted context omitted.

I'm a bit disappointed that we've ended up with Rust in the kernel but not Ada. The kernel relies on GCC and there's already an Ada compiler in GCC, so it wouldn't require adding another compiler as a build requirement like Rust does. There's a couple of major advantages that Ada could have in the Linux over Rust for safe drivers: 1. Having the option to use SPARK for fully verified code provides a superset of the co…

> 2. Representation clauses almost entirely eliminate the need for the error-prone manual (de-)serialisation that's littered all over Linux driver code: Do representation clauses let you specify endianess? From a quick glance at that link it didn't appear so. I would imagine that invalidates most use cases for them.

You can specify endianness, but only over the entire record, not an individual field. The way it works is a little complicated: https://www.adacore.com/gems/gem-140-bridging-the-endianness...

Re: Ada's dependent types, and its types as a whole

#25

Post by TypingOutBugs »

seabird wrote: post #13
TypingOutBugs wrote: post #9

I’d love to work with Ada but never had the opportunity. Anyone know which companies hire for it?

I've seen a single company that does warehouse management software out of Sweden that advertises (in job listings) that they're using it. Otherwise, it's pretty slim pickings if you're not applying in its wheelhouse (high integrity systems -- aerospace, defense, medical, etc). If you do microcontroller firmware development, I'd say it's perfectly reasonable to float it for a smaller project and just give it a spin. T…

What was the company in Sweden? Thankfully I live in Stockholm!

Re: Ada's dependent types, and its types as a whole

#26

Post by timhh »

jonlong wrote: post #15

Coming from the type theory side with only a passing glance at Ada, I am nevertheless sure: this is not what type theorists mean when they talk about dependently typed languages. Such languages derive from the formulation of Per Martin-Löf (also called Intuitionistic Type Theory), they include dependent sum and dependent product types, and they allow type checkers to prove complex statements about code. (The history…

Maybe they're not implying this kind of limited dependent type system but surely it is still dependently typed? It's just not the "full fat" dependent typing.

Another example of a language with limited dependent typing is Sail. It has "lightweight" dependent types for integers and array lengths (pretty similar to Ada from what it sounds like).

It's very good in my experience - it lets you do a lot of powerful stuff without having to have a PhD in formal verification (again, sounds similar to Ada).

> An example of something you can do in a dependently typed language is write a sorting function in such a way that the type checker proves that the output will always be in sorted order.

Yeah you can't do that but you can have the type checker say things like "n^m is positive if n is positive or even" or "foo(x) -> (bits(n), bits(m)) with m+n=x" (not the actual syntax). I'm pretty sure you can't do that stuff in a type system without dependent types right?

Re: Ada's dependent types, and its types as a whole

#27

Post by LiamPowell »

rtpg wrote: post #23
LiamPowell wrote: post #20

Earlier quoted context omitted.

> An example of something you can do in a dependently typed language is write a sorting function in such a way that the type checker proves that the output will always be in sorted order. I am pretty sure this cannot be done in Ada; checking at runtime does not count! It actually can be done in Ada, but not purely with the type system, instead we rely on SPARK, which converts Ada code and passes it through various au…

what is the flow for working through this kind of proof? Is there an interactive proof mode like you find in a lot of dependent type provers? Or is there some other guiding mechanism for telling you that you haven't provided enough guidance with asserts?

SPARK will give you some guidance, but there's no particularly fancy interactive tools. Here's an example of working through a different sorting algorithm: https://blog.adacore.com/i-cant-believe-that-i-can-prove-tha...

Re: Ada's dependent types, and its types as a whole

#28

Post by jonlong »

LiamPowell wrote: post #20
jonlong wrote: post #15

Coming from the type theory side with only a passing glance at Ada, I am nevertheless sure: this is not what type theorists mean when they talk about dependently typed languages. Such languages derive from the formulation of Per Martin-Löf (also called Intuitionistic Type Theory), they include dependent sum and dependent product types, and they allow type checkers to prove complex statements about code. (The history…

> An example of something you can do in a dependently typed language is write a sorting function in such a way that the type checker proves that the output will always be in sorted order. I am pretty sure this cannot be done in Ada; checking at runtime does not count! It actually can be done in Ada, but not purely with the type system, instead we rely on SPARK, which converts Ada code and passes it through various au…

Ah, very interesting. It does seem that the Ada community has done serious engineering work to build in powerful formal verification, in a way that is somehow parallel to the (much slower, for practical purposes, if more elegant) arc of type theory...

Re: Ada's dependent types, and its types as a whole

#29

Post by zerr »

seabird wrote: post #6

Ada is a criminally underrated tool that is unfortunately probably doomed to perpetually take the backseat to Rust despite Rust not solving all the problems Ada does. It's really sad that so many people's idea of safe programming is pretty strictly limited to memory safety, and that because Ada's baseline memory safety (SPARK is a different story) isn't as robust as Rust's borrow checker (in the sense that it doesn't…

The literally verbose syntax contributes to its unpopularity as well. It is extremely hard to skim/read and comprehend prose-like Ada code.

Re: Ada's dependent types, and its types as a whole

#30

Post by shakna »

zerr wrote: post #29
seabird wrote: post #6

Ada is a criminally underrated tool that is unfortunately probably doomed to perpetually take the backseat to Rust despite Rust not solving all the problems Ada does. It's really sad that so many people's idea of safe programming is pretty strictly limited to memory safety, and that because Ada's baseline memory safety (SPARK is a different story) isn't as robust as Rust's borrow checker (in the sense that it doesn't…

The literally verbose syntax contributes to its unpopularity as well. It is extremely hard to skim/read and comprehend prose-like Ada code.

Wouldn't Rust's symbol heavy syntax contribute the same?
Post reply on HN