3 ms·

> And what's the problem with soundness? You can definitely not provide any guarantee for arbitrary DSLs implemented in your system, but claim you do. > I ca

by nmrm2 11y ago

> And what's the problem with soundness? You can definitely not provide any guarantee for arbitrary DSLs implemented in your system, but claim you do. > I can even derive formal proofs for simple DSLs when I have too. Am I looking at the correct thing on GitHub? CombinatoryLogic? I can't find any code here that would suggest you're interfacing with a theorem prover, much less the incredibly amount of machinery that must be involved in taking two correctness proofs and producing a correctness proof for their combination. > Then do not combine these things in the unsound ways. As simple as that. I think this pretty much sums up the contribution here. It's a framework that doesn't face any problems with compositions because you've chosen not to write down things that don't compose well. > If the source language is sound, each of the target languages are sound, and all the transforms in between are sound, then the result is sound and robust. To repeat myself once again, your framework doesn't force any of these to be true. It's just as easy to write down unsound things as to write down sound things. The fact that you choose to write down sound things is nice I guess, but it's not a demonstration of the capacity of the framework or methodology to preserve soundness. It's just a demonstration of your own capabilities... we hope. That works fine and well when DSLs don't get inter-leaved in unexpected ways and are only developed by a small set of developers. But then, we've known how to design DSLs in those cases for a long time. There's no REAL composition going on -- just the sort of combination that's always happened. The actually interesting question is how to support an open world of DSLs. Where composing DSL1 with DSL2 won't break some guarantee that the writer of DSL2 worked hard to achieve. And where even changes to DSLA, which DSL2 depends on, also won't break those guarantees. And where the authors of all three languages never even know each other exist. And not just "if you don't write down the wrong thing", but "because the framework prohibits it". You don't solve this problem. In fact, I can't even figure out how to state some specification of a DSL, much less that it's preserved under a transformation... Again, your framework might be a great setting for doing DSL engineering. And I don't doubt that you designed a tool that's useful for you. But you're making some pretty extreme and apparently over-stated claims beyond "nice framework solving a few practical implementation problems". (Which is a shame because your tool seems nice, but your comments come across (to me) a bit snake-oily, so I'm not sure how seriously I should take the tool / approach. I think if you re-stated your claims so that they're a more accurate representation of the problems you do (and don't) solve, you might get a better reception.)

sklogic 11y ago
> You can definitely not provide any guarantee for arbitrary DSLs implemented in your system, but claim you do. No, I never claimed so. It's a responsibility of a DSL developer, although it is very easy, because of the small size of any practical DSL implementation. > I can't find any code here that would suggest you're interfacing with a theorem prover I did not publish yet a large chunk of work which contains a statically typed version of the host language with an ACL2-like inference engine. It's still quite experimental, but I did many mechanical proofs manually in the past (mostly in the hardware-related DSLs). > much less the incredibly amount of machinery that must be involved in taking two correctness proofs and producing a correctness proof for their combination. I still cannot understand your point. Why exactly a combination of DSLs is going to introduce any additional complexity? I demonstrated in my examples that mixing the DSLs is exactly the same thing as using them. There is a dataflow dependency between various semantic realms, but it is really hard to break any constraints by merely feeding valid data in and getting a valid data out. So, yes, no existing language workbench enforce language soundness, it's up to the designer to ensure the correctness. But, can you name a single general purpose language with an enforced soundness, CompCert aside? > get inter-leaved in unexpected ways Mind providing any examples of this? I cannot think of any interesting case, due to the very nature of this approach, there is no difference between using the languages in a "normal" way and targetting them in code generation. > guarantee that the writer of DSL2 worked hard to achieve What does this guarantee worth if it can be broken by merely using this language? I see that you're more on a bondage&discipline side of the PL research. In this case we have to agree to disagree, my decades of Lisp experience are forcing me to lean the other way. I'm all for the formal proofs and I'm doing them a lot when it is really necessary (e.g., in hardware, where the cost of error is huge and verification capabilities are limited), but besides that, having a hacking and permissive language allows experimentation, while b&d languages inhibit innovative designs. I only built a b&d, non-Turing-complete (total functional), strictly typed version of my language workbench after years of experimenting on a dynamic, unrestricted codebase. So, my claims are: 1) It's dead simple to implement eDSLs using metaprogramming, if you've got the right tools (features for dealing with ASTs and their transforms; examples: Nanopass framwork, Racket in general) 2) If you have a hierarchy of ready-made DSLs, then with the above approach you can easily mix arbitrarily selected properties of all of your existing languages into a new DSL. 3) PEG and GLR are great. The others are inferior. All hail the lexerless parsing! And, btw., my framework is not any different from the other metaprogramming-based language workbenches. You can achieve this ease of development and robustness with any other framework.

by nmrm2 11y ago

sklogic 11y ago

> You can definitely not provide any guarantee for arbitrary DSLs implemented in your system, but claim you do. No, I never claimed so. It's a responsibility of a DSL developer, although it is very easy, because of the small size of any practical DSL implementation. > I can't find any code here that would suggest you're interfacing with a theorem prover I did not publish yet a large chunk of work which contains a statically typed version of the host language with an ACL2-like inference engine. It's still quite experimental, but I did many mechanical proofs manually in the past (mostly in the hardware-related DSLs). > much less the incredibly amount of machinery that must be involved in taking two correctness proofs and producing a correctness proof for their combination. I still cannot understand your point. Why exactly a combination of DSLs is going to introduce any additional complexity? I demonstrated in my examples that mixing the DSLs is exactly the same thing as using them. There is a dataflow dependency between various semantic realms, but it is really hard to break any constraints by merely feeding valid data in and getting a valid data out. So, yes, no existing language workbench enforce language soundness, it's up to the designer to ensure the correctness. But, can you name a single general purpose language with an enforced soundness, CompCert aside? > get inter-leaved in unexpected ways Mind providing any examples of this? I cannot think of any interesting case, due to the very nature of this approach, there is no difference between using the languages in a "normal" way and targetting them in code generation. > guarantee that the writer of DSL2 worked hard to achieve What does this guarantee worth if it can be broken by merely using this language? I see that you're more on a bondage&discipline side of the PL research. In this case we have to agree to disagree, my decades of Lisp experience are forcing me to lean the other way. I'm all for the formal proofs and I'm doing them a lot when it is really necessary (e.g., in hardware, where the cost of error is huge and verification capabilities are limited), but besides that, having a hacking and permissive language allows experimentation, while b&d languages inhibit innovative designs. I only built a b&d, non-Turing-complete (total functional), strictly typed version of my language workbench after years of experimenting on a dynamic, unrestricted codebase. So, my claims are: 1) It's dead simple to implement eDSLs using metaprogramming, if you've got the right tools (features for dealing with ASTs and their transforms; examples: Nanopass framwork, Racket in general) 2) If you have a hierarchy of ready-made DSLs, then with the above approach you can easily mix arbitrarily selected properties of all of your existing languages into a new DSL. 3) PEG and GLR are great. The others are inferior. All hail the lexerless parsing! And, btw., my framework is not any different from the other metaprogramming-based language workbenches. You can achieve this ease of development and robustness with any other framework.