jsmorph

5 ms·

1.
by jsmorph 3mo ago
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 fro
2.
by jsmorph 5mo ago
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
3.
by jsmorph 5mo ago
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/agen
4.
by jsmorph 3y ago
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-patte
5.
Linux Foundation Announces Launch of TLA+ Foundation(linuxfoundation.org)
10 points by jsmorph 3y ago|1 comments
6.
by jsmorph 3y ago
Same. Maybe a GPT-driven super-tactic.
7.
LLM generates some anti-microbial proteins(newscientist.com)
1 points by jsmorph 4y ago|0 comments
8.
Swarm – Low cost, global satellite connectivity for IoT(swarm.space)
230 points by jsmorph 4y ago|156 comments
9.
by jsmorph 4y ago
[0] https://en.wikipedia.org/wiki/Homotopy_type_theory [1] https://homotopytypetheory.org/book/
10.
by jsmorph 5y ago
https://www.inaturalist.org/ also does this kind of thing. iNaturalist works well for lots of different organisms.
11.
Show HN: Sheens: state machines for message processing(github.com)
1 points by jsmorph 8y ago|0 comments
12.
by jsmorph 12y ago
I hope this group can figure out a master contributor license agreement. Getting together N bilateral CLAs is not ideal.
13.
A Bayesian Model for an Increasing Function (using Stan)(blog.davidchudzicki.com)
1 points by jsmorph 13y ago|0 comments
14.
by jsmorph 13y ago
Here's a colorization based on compositeness: http://blog.morphism.com/2010/05/building-numbers.html
15.
OpenCL and the 13 Dwarfs(synergy.cs.vt.edu)
4 points by jsmorph 13y ago|0 comments
16.
Pharo: A malleable and powerful platform(slideshare.net)
87 points by jsmorph 13y ago|50 comments
17.
Using The Dec Alpha As A Programmable Micro-engine (1994)(pt.withy.org)
1 points by jsmorph 13y ago|0 comments
18.
by jsmorph 16y ago
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.