4 ms·
> Dependent types are the future I think so too. Having a solver fill in my program from the proof obligations is way too amazing. I feel like there could be a
by agentultra 10y ago
> Dependent types are the future
I think so too. Having a solver fill in my program from the proof obligations is way too amazing. I feel like there could be a connection from high-level specification -> implementation either by proof obligation or possibly synthesis via this route.
Plus I like ML/OCaml and would be happy to see more of it in the world.
- tennix 10y agoAgreed on dependent type, and I also love ML syntax more than haskell(yes I don't like indentation sensitive language). BTW I suggest you give FStar a try, it has dependent type and OCaml/F# like syntax and support theorem proving
- pklausler 10y agoYou don't have to use indentation for nesting in Haskell. Haskell's syntax is actually defined with curly braces and semicolons and you're free to use them. It's just smart enough to add missing curly braces and semicolons at the right places according to indentation when they're missing.
- tennix 10y agoYeah, you're right. But almost all of the community uses indentation which defined as layout in Haskell2010 Language Report instead of semicolons and curly braces