News for hackers. Stuff that matters.

A comment on Leanstral: Open-Source foundation for trustworthy vibe-coding. Parent comment

Re:Leanstral: Open-Source foundation for trustworthy vibe-co... by cjfd on Tuesday March 17, 2026 @04:13AM (#47409870)
Well, if you do not need to care about performance everything can be extremely simple indeed. Let me show you some data structure in coq/rocq while switching off notations and diplaying low level content.

Require Import String.

Definition hello: string := "Hello world!".

Print hello.

hello = String (Ascii.Ascii false false false true false false true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true true false true true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false false false false true false false) EmptyString))))))))))) : string

[ Parent | on HN ]
Re:Leanstral: Open-Source foundation for trustworthy vibe-co... by strongly-typed on Tuesday March 17, 2026 @09:25AM (#47412323)
You know you could just define the verified specs in lean and if performance is a problem, use the lean spec to extract an interface and tests for a more performant language like rust. You could at least in theory use Lean as an orchestrator of verified interfaces.
[ Parent | on HN ]
Re:Leanstral: Open-Source foundation for trustworthy vibe-co... by d_christiansen on Wednesday March 18, 2026 @03:18AM (#47422550)
In Lean, strings are packed arrays of bytes, encoded as UTF-8. Lean is very careful about performance; after all, a self-hosted system that can't generate fast code would not scale.
[ Parent | on HN ]