[–] hargup 16d ago ↗ I belive we can do regular software much better using formal methods, and I want to better communicate the developing tools, learnings and methodology.Would appreciate a quick reaction from the community. [–] [dead] taoh 13d ago ↗ [dead]
[–] eliasdejong 13d ago ↗ > typed databases let you express queries which are just super hard to express otherwiseIsn't type validation already in SQL with `CHECK` constraints? I don't see what the language is adding here exactly. [–] [dead] hargup 8d ago ↗ [dead]
[–] alex7o 12d ago ↗ This sound very similar to https://www.geldata.com/ you might want to check it out. [–] hargup 8d ago ↗ Thanks, looks interesting.
[–] nylonstrung 12d ago ↗ This is cool, I have been working on something similar with Lean4 albiet focused on compiling to SubstraitThis is pretty well done as well https://github.com/palladin/lean-linq
9 comments
[ 4.2 ms ] story [ 46.2 ms ] threadWould appreciate a quick reaction from the community.
Isn't type validation already in SQL with `CHECK` constraints? I don't see what the language is adding here exactly.
This is pretty well done as well https://github.com/palladin/lean-linq