HackerTrans
热门最新趋势评论往期问答秀出招聘

jsmorph

no profile record

评论

jsmorph
·22天前·讨论
Cool. I've been working on a compiler for a subset of Lean that targets WASM. The compiler is implemented in Lean.

https://github.com/jsmorph/leanexe

I think I managed to use Talos to prove the WAT generated from an example LeanExe program is correct. ?

https://gist.github.com/jsmorph/275a15dc21af037e1d02a1b433be...

Fun.
jsmorph
·3个月前·讨论
Re 1: Discussing and guiding the desirable theorems for general-purpose programs has been a major challenge for us. Proofs for their own sake (bad?) vs glorious general results (good but hard?). Actual human guidance there can be critical there at least for now.
jsmorph
·3个月前·讨论
Slightly off topic: This project https://agentcourt.ai/arb/analysis/index.html uses a Go/Lean hybrid design. The Go code is mostly glue, and the Lean code is the logic https://github.com/agentcourt/adjudication/tree/main/arb/eng.... It's not math-intensive. Really just functional programming with some interesting proofs (including soundness ideally). Go code can migrate to Lean code when that makes sense.