Proof.

[funarog]

Since the LSP is written in IDRIS, can it then be proven that the LSP adheres to the LSP 3.17?

[andorp]

To have a proof about the correctness of the implementation of the LSP, first we need to have the LSP formalized [1] that can be easily translated to Idris. If we have that we could start to think about how to match the actual implementation and the correctness proof.

I think @ShinKage original dependently typed approach is good enough for the current state of the LSP, which is really a part-time project with low priority for many of us. For me personally, I couldn't invest time to formalize the LSP protocol and refactor the LSP to respect such a construct.

[1] Do you know if such a thing exist? Although by the size of the protocol I think that would be a big (or even a research) project.

[funarog]

Yes the LSP Specification exists: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/. But I am sure you knew that. A specification that is easily translated or a language that supports representing specifications is the crux of software development. From a preliminary review, I believe the Idris LSP can be structured to match the LSP specification. I was surprised that it was not. I strongly disagree that the Idris-LSP is "good enough." It is a full time project for me to find a programming language that can helps a developer verify that requirements are being implemented. I also disagree that it would be a research project. As I said after conducting a preliminary review, I was surprised to see that the Code did not resemble the specification. And the reason it surprised me is because it looked a reasonable approach to follow the LSP specification. It would also demonstrate that a type driven development can verify (prove) that it has implemented a set of requirements.

[andorp]

A specification that is easily translated or a language that supports representing specifications is the crux of software development.

Yes, I agree to some extend. The LSP currently has the specification in plain English, which is I am not sure that easily translates to constructive logic. See below.

I strongly disagree that the Idris-LSP is "good enough."

I didn't say that the LSP implementation is complete and we shouldn't improve it. It needs a lot of improvements, but currently it matches and in some sense supersedes the current capabilities of the Idrsi2 compiler.
The type abstraction that @ShinKage created for this project in my eyes is good enough. It helped me contribute to this project.

It is a full time project for me to find a programming language that can helps a developer verify that requirements are being implemented.

I am really happy for your position. Maybe you can help the Idris-LSP along the way.

I also disagree that it would be a research project.

What I meant by this point, is that LSP is currently defined in form of a natural language. When we do constructive proofs we need to have a rigid rule based formal system with logical statements about the subject being formalized. Such a system can be modeled as data families in Idris. The next step is the certified implementation which shows that the data (or operational trace) matches the formal specification. But we miss the first piece of this puzzle.
I don't know any of such formalization of the LSP protocol. The natural language description isn't suitable to translate mechanically to indexed data families in Idris.

I know of a similar project that formalized WebAssembly specification in a theorem prover (and found inconsistencies) was presented in several academic and industrial conferences and was backed by financial contributions from different sources.

First formalizing the LSP protocol than sketching an implementation based on that is an option, but it needs a completely different dynamics the current LSP development effort has. The current implementation is brought together with people sacrificing their free time in a collective effort to mirror the IDE capabilities of the Idris2 compiler.

I was surprised to see that the Code did not resemble the specification

Can you point us to any other LSP implementation that fulfills this requirement?

And the reason it surprised me is because it looked a reasonable approach to follow the LSP specification.

Yes, I completely agree if this project would be backed financially and the contributors would work on it full time. I have to stress that I think when @ShinKage laid down the foundations did a great job there. And it was good enough for us to port the IDE commands from the Idris2 compiler, resulting a server which is able to talk to an LSP client consistently. And yes the architecture could be way better / completely different, but that would also mean different project structure and different real life constraints too.

It would also demonstrate that a type driven development can verify (prove) that it has implemented a set of requirements.

Yes that would be great. But the main question, who would have the resources to translate the LSP informal definition to a formal system? Can you help with that?

I think the diverging point in our discussion is that 'a specification is easily translated' . I think anything that is longer than 10+ pages of plain English won't be easy to work with, no matter the target language, and it would need a full time focused effort.

I am sure, if your company would support someone financially the LSP could satisfy the standards of your company too.

[ShinKage]

Can you give an example of what you mean by "can be structure to match the LSP specification". For example, the datatypes in Language.LSP.Message are not automatically derived from the textual specification but were built to match exactly the 3.16 specification and I'm (slowly) porting the 3.17 specification. Another example is that, the type of the request handling function is written such that you must return the correct response message according to the specification.
I think @andorp was asking if there was a formalization of the protocol in a specification language or in some theorem prover instead of the well-known natural language specification.

[andorp]

Thank you for porting the 3.17.

[andorp]

I think @andorp was asking if there was a formalization of the protocol in a specification language or in some
theorem prover instead of the well-known natural language specification.

Exactly

[funarog]

Thank you , you have answered my question. My goal is to bring natural language requirements and natural language specifications into software design. Type Driven Development appears to be an excellent programming language to support that effort. So the majority of my effort is to see if it can be accomplished.

---

That is quite a list of questions.
I contemplated jumping in and assisting in the development of the Idris2-lsp project. However, when I saw that the Server.Main had about 30 dependencies (imports), that Server. Capabilities are dependent JSON. I was expecting perhaps a Microservices Architecture Pattern. But I couldn't figure what architectural pattern was used. Also, the current protocol specification defines that the lifecycle of a server is managed by the client, this also took a bit of of jumping around to figure out how that specification was implemented. So, to be frank, I decide not to become involved. I saw too many anti-patterns to suit my taste. Although I could work full time on the project. Mind you. I can see a lot of work has gone into the project. And don't mean to minimize the effort. IT is not an easy effort, especially if it is only being worked on part-time. But, for the time being I will use the Idris2 --ide-mode and Nvim

It is highly unlikely one will ever see a formal specification for LSP, e.g. Z notation. I am sure we all know that software requirements are almost always provided in a natural language format. It is very common for the software team to develop an architecture and a model of the design space based on these natural language descriptions of Concepts of Operations, Requirements and verification Criteria. Of which, puts the burden onr the software team to structure the design in a manor that others can quickly understand Nonetheless, the LSP specification is typical of the amount of detail with which software developers have to work. Make specification more machine-readable.

I can offer one paper I have read with regard to LSP: Editing Support for Software Languages: Implementation Practices in Language Server Protocols Section 4.3 Concern: Structuring Servers. I would have probably started there. Or set up a plan to migrate. Towards a Language Server Protocol Infrastructure for Graphical Modeling. I also looked at the agda-lsp and haskell-lsp. They were easier to follow.

[andorp]

My goal is to bring natural language requirements and natural language specifications into software design.

I would like to see this a lot. I worked as a QA engineer too at some point in the past and I find this topic fascinating.

Type Driven Development appears to be an excellent programming language to support that effort

With dependent types we can model first order logic, any language model which fits there could be applied, but we still need to have a semantic model to interpret any sentence structure. If you know of any references please share.

I answer the questions in the order of appearance.

I was expecting perhaps a Microservices Architecture Pattern.

At this point unfortunately no real architecture is designed for the LSP. @ShinKage laid down the foundations and we jumped on the IDE commands adding them one by one. No architectural discussions were happening, no real architect person was behind the current codebase. The first version of the LSP only supported one file at a time. This was extended later on, but also without any architectural considerations.

But I couldn't figure what architectural pattern was used

That is not surprising, for me it feels it has none.

Also, the current protocol specification defines that the lifecycle of a server is managed by the client, this also took a bit of of jumping around to figure out how that specification was implemented.

I am not sure about the life-cycle, but I would think this is probably scattered through the code and only exists in the implicit state transitions. If this is the case, I agree that could use some dependently typed love.

So, to be frank, I decide not to become involved.

I can understand that, but I am a little bit saddened by it.

I saw too many anti-patterns to suit my taste.

Evolutionary architecture. As in the "Design It!" book tells us, if we don't do architect consciously we will have the architecture we don't like. We could discuss these points, as I want to learn about the scary parts for others that should be improved. When my time, mood and other responsibilities allow I feel contributing to the LSP and steer it into a more community project direction.

IT is not an easy effort, especially if it is only being worked on part-time

Thank you. And the part-time is way exaggerating, I would call it on-and-off contributions. If you check the commit history it is mainly updating the Idris version and keep afloat the existing code.

But, for the time being I will use the Idris2 --ide-mode and Nvim

What is the user-experience or use case where Idris-LSP does not fit your workflow?

It is highly unlikely one will ever see a formal specification for LSP, e.g. Z notation.

Yes, I agree.

Of which, puts the burden on the software team to structure the design in a manor that others can quickly understand

• Yes, I agree. And the Idris-LSP currently has no team, in a software project sense.
• As an addition such requirements are formalized in form of test suite by the QA team or the developer team. So some kind of specification exists. But certified programming requires a model that can be formalized via constructive proofs.

I can offer one paper I have read with regard to LSP

Thank you for the reference.

I also looked at the agda-lsp and haskell-lsp. They were easier to follow.

I didn't know about the agda-lsp. I've just looked at it and it seems it is written in Haskell. I assume that it probably piggybacks on the haskell-lsp server libraries/tools.

It is understandable that the haskell-lsp is easier to follow and does things nicer, but that is comparing apples to oranges situation. The Haskell-LSP is many year long project and it is backed by Meta/Facebook and its Haskell Developer-eXperience team. I think Idris-LSP has less than 2 man months put into it. If we wanted to have a fare comparison (that we don't want to do) we would need to check the version of Haskell-LSP after its second month and check its state.

Thank you for your thoughts, they really support my feeling that the Idris-LSP needs code cleaning and acrhitectural improvements, even if it will be far away from the formally verified implementation.

[funarog]

Well I am glad my first impressions were not off the mark. I certainly did not want to dismiss the amount of work that had been accomplished.
If I find that nvim+idris2 --ide-mode doesn't work out for me, I may come back to the idris2-lsp. Because it would give me an opportunity to see how well natural language requirements can be incorporated into ... as the TDD book claims: "types as being a plan, with the type checker acting as your guide, leading you to a working, robust program."

I have been trying to get through the TDD book, but got sidetracked with nvim, vscode and idris2-lsp.