@rahulc29 @isAdisplayName Yes... And also, I think that there is a pretty huge spectrum of what "production" means to different people. There are some definitions of "production" under which I could certainly use Idris — and ultimately the difficulties would be very similar to those one would encounter in a non-dependently typed language that hasn't had zillions poured into it by Facebook or Google or Apple.
I think in nearly all these cases, what prevents something from being usable "in production" is not so much language features & kinks & compiler bugs, but the lack of an ecosystem.
=> More informations about this toot | View the thread | More toots from jonmsterling@mathstodon.xyz
=> View rahulc29@mathstodon.xyz profile | View isAdisplayName@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).