Would it be better to build dependent types into the language itself so that we can guarantee any spec we want? Or do these tools have some advantage over dependent typing?

▲

Ericson2314 8 months ago | parent | next [-]

From glancing at https://www.andrew.cmu.edu/user/bparno/papers/verus-ghost.pd... it is more related than you think.

- The various "modes" are going to be needed either way, because side-effectful functions at the type level are a research problem that probably isn't worth the effort.

- The in the pure functional "promotable" fragment, it probably also makes sense to relax aliasing rules / have infinite number types / etc. because all the stuff is going to compile away anyways.

I hope projects like this catch on, and incentivize Rust getting a stronger type system, because the benefits will flow in both directions.

	▲	daxfohl 8 months ago \| parent [-]
		Oh wow, that's incredibly cool. (tldr: the authors of Verus, mostly university researchers, are already thinking in this direction). I think having guardrails like this is going to incredibly important as AI code gen starts taking a bigger role. Hopefully, as a separate comment mentioned, there can be a standard created so that AI tools can learn it more easily.

▲

pcwalton 8 months ago | parent | prev | next [-]

My feeling is that dependent types add complexity to a language that's already well-known for having a complex type system, so I'm nervous about blowing the complexity budget. But I'm bullish on tools like Verus, Prusti, and Creusot because they allow people who need to write low-level unsafe code to prove their code safe, while keeping the complexity of the safety proofs localized to that code, so most Rust programmers don't need to worry about it. This allows verification of Rust code without surfacing complexity to most developers. We can have our cake and eat it too.

	▲	vacuity 8 months ago \| parent [-]
		Agreed. Rust is on track to becoming a practical language for many verification projects. If necessary, perhaps a dialect that focuses on verification could be made and separately maintained (it would probably cut out a lot of normal Rust), or one would just switch to a different technology.

▲

jerf 8 months ago | parent | prev [-]

I am not aware of a viable "dependent type system". Such ones as we have are very complicated and not generally a good engineering trade off.

It is The Dream in some ways, but it is much, much easier said than done.

▲

Ericson2314 8 months ago | parent [-]

We've head them for 20 years. Lean is getting a lot of attention. Dependent types are not very complicate --- proofs are very complicated, but that is inherent. Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.

▲

jerf 8 months ago | parent | next [-]

I'll cop to the word "viable" doing a lot of heavy lifting there, but I have not yet seen a dependent typing system that is adequate for engineering work. There are research systems, yes, and there are many people doing laudable work on it, but when people on HN pine for "dependent type systems", I think they're talking about wanting to live in a world where most people who are programming today are instead programming in dependently-typed systems happily and productively, not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages.

Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.

I'd also say that "hey, you can use this dependently-typed language, just don't try to actually use the dependently-typed features" is also not what people are pining for.

	▲	Ericson2314 8 months ago \| parent [-]
		> not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages. Well, to be fair, I would not cry if this happened. > Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical. I wrote a tic-tac-toe in Lean. https://github.com/Ericson2314/lean-tic-tac-toe/. Yes, it took me far longer than I would have in Haskell, but that is just because: 1. Unfamiliarity with the standard library, tooling etc. I didn't expect Applicative to be in mathlib not batteries, for example. 2. I tried to prove things I wouldn't have in the Haskell version If I knew the standard library, and did plane old arbitrary-length lists and partial (bounds-checked) indexing with arbitrary nats, I would have had less fun, but also done things way faster. I am excited for the latest Machine-Learning tactics or whatever too, but the idea that "everything is going to do something they didn't before (proofs) and it will be no harder" is not a goal I am aiming for. Proofs will always be a trade-off between up-front costs and fearless refactoring on an ongoing basis. That's OK! I don't expect magic, I just want my programming language to give me the full spectrum of options, and then I can make my own economic decisions.

▲

zozbot234 8 months ago | parent | prev [-]

> Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.

I have to disagree with this, since fully general dependent types seem to inherently involve a kind of compile-time evaluation. You can recover a sort of phase distinction (i.e. a post-compile "run time" phase) but only AIUI through an "extraction" step that dispenses with the actual dependently typed parts of the program.

	▲	Ericson2314 8 months ago \| parent [-]
		> You can recover a sort of phase distinction Yes the literature says how to do this. It's not hard. Any program that could be written in something weaker like System F will have the same erasure. > inherently involve a kind of compile-time evaluation. compile-time evaluation doesn't pose a phase-separation problem. Indeed, nothing to the right of a `:` will ever need to be evaluated on runtime.