[boxfire]

Programming in dependent types with univalence (Homotopy Type Theory) is an awesome way to see this realized.

The typing statement has to be proven by realizing the isomorphism demanded by substitution. You are more than anything directly proving what you claim in the type. Since proof is isomorphism here, the computation in terms of lowering the body of the definition to a concrete set of instructions is execution of your proof! (possibly machine code or just abstract in a virtual machine like STG). The constructive world is really nice. I hope the future builds here and dependent types with univalence is made easier and more efficient.

[js8]

What specific system (programming language) do you recommend to try this?

[codekilla]

For dependent types, I would look at Idris [1]. Adding Univalence in a satisfying way is I think still somewhat of a research question (I could be wrong, and if anyone has any additional insight would be interested to hear), i.e. see this thread about Univalence in Coq [2]. There are some implementations in Cubical Type Theory, but I am not sure what the state of the art is there [3]

[1]https://www.idris-lang.org [2]https://homotopytypetheory.org/2012/01/22/univalence-versus-... [3]https://redprl.org

[AnimalMuppet]

This is not going to catch on any time soon.

Assume that regular software has, on average, one bug every 50 lines. (All numbers made up on the spot, or your money back.) Let's suppose that Idris can reduce that to absolutely zero. And let's suppose that totally-working software is worth twice as much as the buggy-but-still-mostly-working slop we get today.

But Idris is harder to write. Not just a bit harder. I'd guess that it's maybe 10 times as hard to write as Javascript. So we'd get better software, but only 1/10 as much of it. Take your ten most favorite web applications or phone apps. You only would have one of them - but that one would never crash. Most people won't make that trade. Most companies that produce software won't make it, either, because they know their customers won't.

Well, you say, what about safety-critical software? What about, say, airplane flight control software? Surely in that environment, producing correct software matters more than producing it quickly, right?

Yes, but also you're in the world of real-time embedded systems. Speed matters, but also provably correct timing. Can you prove that your software meets the timing requirements in all cases, if you wrote it in Idris? I believe that is, at best, an unsolved problem. So what they do is they write in carefully chosen subsets of C++ or Rust, and with a careful eye on the timing (and with the help of tools).

[jfoutz]

I've been dabbling with Idris and agda and coq. I think I'm pretty much settling on agda, because I can appeal to Haskell for help. It's tough finding things that aren't just proofs, actually running a program isn't hard, there just doesn't seem to be many people who do it. I've got some toy projects in mind, and I'm going to lean hard on https://github.com/gallais/aGdaREP (grep in agda). I can't tell you if it's ten times harder - that seems high. It's different, sure. I'm having a tougher time than with, say, prolog. But most of the bumps and bruises are from lack of guidance around, uh, stuff.

So given that context, it doesn't sound to tough to add a cost to the type for each operation, function call, whatever, and have the type checker count up the cost of each call. So you'd have real proof that you're under some threshold. I wouldn't put the agda runtime on a flight control computer. But I think I could write a compiler, now, For like a microcontroller that would count up (or spend time budget, doesn't matter).

A more sophisticated computer would be way way harder, and be resource efficient. But if you modeled it as "everything's a cache miss" and don't mind a bunch of no-ops all the time, that would be a pretty straightforward adaptation of the microcontroller approach.

[siknad]

I would recommend trying Lean4 because I think it is better suited to programming. Lean has Rust-like toolchain manager; a build system (cf. `.agda-lib`); much more developed tactics (including `termination_by`/`decreasing_by`); more libraries (mathlib, and some experimental programming-oriented libraries for sockets, web, games, unicode...); common use of typeclasses in stdlib/mathlib; `unsafe` per declaration (cf. per module in Agda); sound opaque functions (which must have a nonempty return type) used for `partial` and ffi; "unchained" do-notation (early `return`, imperative loops with `break`/`continue`, `let mut`); easier (more powerful?) metaprogramming and syntax extensions. And in Agda you can't even use Haskell's type constructors with type classes (ex. monad polymorphic fns, and that makes it more difficult to make bindings to Hs libs, than to C libs in Lean).

There are features in Agda/Idris (and probably Coq, about which I sadly know almost nothing) that are absent from Lean and are useful when programming (coinduction, set omega, more powerful `mutual`, explicit multiplicity, cubical? etc), but I'd say the need for them is less common.

[__MatrixMan__]

> So we'd get better software, but only 1/10 as much of it

How much software do you think we need? 10x less sounds about right to me.

[galaxyLogic]

You can produce formally verified software with more expense than Java-Scripting. But is it software that does what we need it to do?

Verification proves that software works according to its "spec". But is the spec "correct"?

Writing NON-formally-verified software 10 x faster means you have a much better chance of figuring out how you should fix your spec.

[haltist]

It should be possible to embed cubical type theory in Idris.[1][2]

1: https://arxiv.org/abs/2210.08232

2: https://chat.openai.com/share/aadb7a0a-08a4-4951-b877-cb2f61...

[logicchains]

IntelliJ Arend probably has the most comprehensive support for HOTT among the proof systems: https://arend-lang.github.io/ . Not a lot in the way of tutorials though, just the official documentation.

[gylterud]

Agda is a nice language with a good homotopy type theory library based on the univalence axiom called agda-unimath.