jsmorph

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.

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.

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.

The section [0] on pattern matching [1] was an important inspiration for some pattern matching that's running in large-scale production today [2].

[0] https://norvig.github.io/paip-lisp/#/chapter5?id=_52-pattern...

[1] https://github.com/norvig/paip-lisp/blob/main/lisp/patmatch....

[2] https://github.com/Comcast/sheens#pattern-matching

Same. Maybe a GPT-driven super-tactic.

[0] https://en.wikipedia.org/wiki/Homotopy_type_theory

[1] https://homotopytypetheory.org/book/

https://www.inaturalist.org/ also does this kind of thing. iNaturalist works well for lots of different organisms.

I hope this group can figure out a master contributor license agreement. Getting together N bilateral CLAs is not ideal.

Here's a colorization based on compositeness:

  http://blog.morphism.com/2010/05/building-numbers.html

Similar visualizations here:

  http://blog.morphism.com/2010/05/building-numbers.html
  http://blog.morphism.com/2010/07/pdfs-from-building-numbers.html

That stuff was generated using Mathematica.