Oh nice. Just found 2 #rustlang nightly features which look like they might bring us closer to one of the two major type level things Iam missing hard in #rust : "extistenia types" (the other one are #GADT)
type_alias_impl_trait:
https://doc.rust-lang.org/unstable-book/language-features/type-alias-impl-trait.html
impl_trait_in_assoc_type:
https://doc.rust-lang.org/nightly/unstable-book/language-features/impl-trait-in-assoc-type.html
Red-black tree in Lean 4 prover.
I proved all needed properties, for example that resulting tree is sorted.
I implemented one operation only: insertion. And I "cheat" by assuming that original tree is always black. My goal was not implementing everything, I just wanted to implement one simple operation and prove really everything about it.
Proof of sorting (insert_sorted) turned out to be rather big. If someone knows how to make it smaller (possibly using mathlib), then, please, tell me that.
I proved all needed properties, for example that resulting tree is sorted. I implemented one operation only: insertion. And I "cheat" by assuming that original tree is always black. My goal was not implementing everything, I just wanted to implement one simple operation and prove really...
https://react-book.melange.re/intro/
I love #ocalm.
it has many superpowers
- #soundcomplete and #strong #typesystem with #typeinference
- #algebraiceffects
- #algebraicdatatypes
- #GADT
- #patternmatching
- pragmatic by default #immutanbility
- pragmatic and optional laziness
it gives confidence and correctness via type system and compiles
#ocaml shape languages like #scala and #rust also #Fsharp is just reincarnation of ocaml for dotnet
Melange brings this power to #reactnative developers.
🇫🇷 L'année passée, j'ai décris un usage du GADT `Eq` pour implémenter des méthodes gardées (et résoudre les méthodes `sum`, `prod` et `flatten`) en préservant la sémantique d'envoi de message !
alios
Askar Safin
vp
Xavier Van de Woestyne
arguil
xameer