GitHub is already using the well-known pure functional language Haskell for the GitHub Semantics project. Other giant companies are using technologies related to category and type theory, functional programming, lambda calculus, etc... as well. However dependently typed languages like F* or Idris are still in the research domains and haven't yet entered in the technology stack of the giant corporations for actual business solutions, nor are adopted in the developer communities.
Do you think such languages will ever be widely adopted by the developers as a robust mathematical solution for developing software? And if yes, how long will it take for companies like GitHub to embrace them just like they went with Haskell for Semantics?
GitHub is already using the well-known pure functional language Haskell for the GitHub Semantics project. Other giant companies are using technologies related to category and type theory, functional programming, lambda calculus, etc... as well. However dependently typed languages like F* or Idris are still in the research domains and haven't yet entered in the technology stack of the giant corporations for actual business solutions, nor are adopted in the developer communities. Do you think such languages will ever be widely adopted by the developers as a robust mathematical solution for developing software? And if yes, how long will it take for companies like GitHub to embrace them just like they went with Haskell for Semantics?