3 ms·
It's on Github after Google Code shut down, but progress is nonexistent since I got sidetracked trying to prove the type-system and type-inference algorithm wor
by eli_gottlieb 10y ago
It's on Github after Google Code shut down, but progress is nonexistent since I got sidetracked trying to prove the type-system and type-inference algorithm work in Coq. I encountered so many errors in my own reasoning about that damn thing that I decided to not accept anything less than a formal proof.
My willpower is wearing down, considering the effort it takes to achieve a full Coq development of something serious like that.
- nickpsecurity 10y agoWell, that's quite an honest assessment. Also supports the value of things like Coq in catching errors. Sorry to hear you're getting bogged down in them. Have you thought about canceling it for something less ambitious that extends top-tier, existing work or merges a few components together? Quite a lot of work out there that can benefit in real-world development that could use some extension or even fixing up of implementations.
- eli_gottlieb 10y agoCurrently, I aim to get the proof development complete in my Copious Free Time and publish a small paper detailing it regarding something more like an extension to Haskell or SML than a complete language of my own. I also have a friend who's trying to Solve Programming Languages by building a dependently-typed systems programming language with modules and type-classes and such, so I can pass him the code and proofs if I really so burningly desire to see my work "ship" somewhere, somehow.
- nickpsecurity 10y ago"regarding something more like an extension to Haskell or SML than a complete language of my own." Smart. Might work out. " building a dependently-typed systems programming language" I've seen a few of those: ATS, Idris, Bedrock in a way. Has your friend published any work showing off his? Or is it still in pre-alpha development?