alt Hacker NewsDetachHead (maintainer of basedpyright) has criticized the TSP before:
- https://docs.basedpyright.com/v1.40.2/type-server/
- https://github.com/microsoft/pylance-release/discussions/718...
Ty (the type checker maintained by astral) however will apparently support the TSP: https://github.com/astral-sh/ruff/discussions/23432
I think the only way MS knows how to make money is lock someone into an ecosystem. I think their next attempt should be a closed source lean checker that has will have proprietary code for NL -> lean formalization checker.