Re:Parse, Don't Validate and Type-Driven Design in Rust
by dernett on Saturday February 21, 2026 @04:06PM
(#47104760)
Not sure about Idris, but in Lean `Fin n` is a struct that contains a value `i` and a proof that `i < n`. You can read in the value `n` from stdin and then you can do `if h : i < n` to have a compile-time proof `h` that you can use to construct a `Fin n` instance.
[ Parent
| on HN ]
Re:Parse, Don't Validate and Type-Driven Design in Rust
by smj-edison on Saturday February 21, 2026 @09:17PM
(#47107437)
I've heard this can be a bit of a pain in practice, is that true? I can imagine it could slow me down to construct a proof of an invariant every time I call a function (if I understand correctly).
Re:Parse, Don't Validate and Type-Driven Design in Rust
by jaggederest on Sunday February 22, 2026 @01:14AM
(#47108688)
I haven't worked significantly with lean but I'm toying with my own dependently typed language. generally you only have to construct a proof once, much like a type or function, and then you reuse it. Also, depending on the language there are rewriting semantics ("elaboration") that let you do mathematical transformations to make two statements equivalent and then reuse the standardized proof.