8 ms·

Ask HN: Any logic based software dev tool which helps building code gradually?

46 points by pezo1919 7y ago

I am missing some tooling for years. My main idea is that as a programmer what I do is constantly reducing the set of all programs to a particular program which satisfies the specification. (At least that is what I think I should do to get a flexible codebase where adding/removing quasi orthogonal constraints is easy: that is where declarative/logic programming, Prolog, rules / inferring assistants come to my mind.) When thinking, reasoning about timing, concurrency, async, correctness happens 1. Step by step, gradually 2. using nothing but logic. We have some tools: eg. type systems to express interdependence (constraints) and they are also useful in that "step by step" gradual manner: it warns me if I misstep, but there is much more information I could get from a "dev assistant". When I am thinking I (have to) enumerate all the possible cases for a given scenario, but I can't really reuse the existing logic statements I have (or ever had!) in my mind, because usually the code is not written in logic and neither the environment processes it to give me insights. Eg. I would like to make logic statements on the ordering of method calls (or basically just events) to make sure it won't conflict with another ordering (there must be at least one ordering which satisfies for all). I would like to toggle on and off my logic constraints to have the currently relevant ones only (to help me to develop other parts of the system), save the sets as "views" and combine them to see if there is any conflict between their related logic statements (and if so I could see what and I could fix it). I'd need higher order logic (eg. existential operator) to make statements about my "desired" program: to help/assist my future self not to forget about that "constraint". Are you aware of such an IDE/tool/project? Agda, Coq, etc might do something similar I just did not realize. I would really appreciate your help, I'm totally obsessed with that.

xhgdvjky 7y ago
tla+ solves a similar problem but isn't exactly what you're describing
- pezo1919 7y ago
  Yes, thanks for mentioning. It has been on my radar as well, but as I have seen its less universal and more focused on the verification of concurrent processes - which is not the whole picture. But I will give a shot if there is nothing else.
  - pron 7y ago
    TLA+ is just as good for non-concurrent stuff. It's just that it's one of the only things capable to naturally tackle arbitrary concurrency, so it gets more focus there.
    - pezo1919 7y ago
      Good to know ty! What are the main differences (pros/cons) using TLA+ vs Dependent Types (and proving the algorithm is fine) for system verification?
      - pron 7y ago
        There are many subtle and less subtle differences, but the main difference is that TLA+ is being used in the industry to help design complex systems in various domains and of various scale, both hardware and software, while dependent types are still in research, and I am not aware of any project not done by a research institution or with the assistance of one to specify and verify a real world system using dependent types in any form resembling ordinary software development and with similar budgets. I am also not aware of any software deeply specified and verified with dependent types that exceeds a few thousand lines of code.
        pezo1919 7y ago
        Ah okay, thanks! The complexity of Asynchronicity & Concurrency lead me to the formal expression of time related logic: Temporal Logic (https://en.wikipedia.org/wiki/Temporal_logic https://en.wikipedia.org/wiki/Temporal_logic) There are multiple temporal logics with different level of usefulness. (Check Temporal logics section.) I really want to solve harder problems and express deeper relations, so it seems to me what I’d need is CTL at least (https://en.wikipedia.org/wiki/Computation_tree_logic https://en.wikipedia.org/wiki/Computation_tree_logic). I thought I might want to model my software (any kind of app!) and prove it is working as intended using CTL (or other more expressive TL) in Agda/Idris (Coq/TLA+) and then make a similar implementation in another language. Eg. there is an LTL implementation in Agda, but I did not find similar things for CTL.(https://github.com/xekoukou/LTL https://github.com/xekoukou/LTL) What do you think, is it a good idea to express my model using (C)TL in Agda/Idris, or I should use a more dedicated piece of technology for that problem? Is there a limit in case of Agda/Idris for that in theory? Any resource is appreciated!
- RBerenguel 7y ago
  Alloy as well, if you are just trying to reduce search spaces.
  - pezo1919 7y ago
    Did not know about it, ty.
- pezo1919 7y ago
  Thanks!
TheAsprngHacker 7y ago
Your post is very vague, but Agda and Coq use types to help you gradually write definitions. Agda has "typed holes," where you specify the goal type and the IDE (Agda Emacs mode) will show you the relevant bindings in scope. Then, you gradually refine your definition, filling in the hole while creating new holes. Thus, Agda lets you "fill in the blank" using types as a guide. Similarity, Coq has a tactic language that builds terms, and you can see what goals there are left to fulfill and write tactic programs interactively. Agda and Coq are pure functional languages, and their type systems are a consistent logical system. They are more mathematically oriented and may not be what you want. Agda Emacs: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.htm... Coq Tactics: https://coq.inria.fr/refman/proof-engine/tactics.html https://coq.inria.fr/refman/proof-engine/tactics.html
- pezo1919 7y ago
  Thanks, dependent typed languages seem something to consider. Coq, Agda and Idris seem the most useful to me.
- Smaug123 7y ago
  Hole-based programming is something I really miss in every non-Agda language I've ever used. In particular, I code professionally in F# in such a way that it should very often be possible for the type-checker to fill holes (or at least to help me fill holes) - lots of annotations, tiny-types to encode more meaning into the types, and so on. Once you've tried agda-mode, you feel hamstrung in every other environment.
  - pezo1919 7y ago
    Yes this is one main feature what I am looking for. I have just replied to another comment where I mention holes but ask a more concrete question about focusing different parts of the system when you have multiple holes. Can you please examine it? Off: may I ask how did you end up with F# and how old are you? I can't really decide the average age of programmers who do know dependent types.
akkartik 7y ago
When you say 'tool', are you thinking of something language-independent? That seems hard. Many questions are impossible to answer in C, for example. Even if other languages are easier, each language would require some fairly specialized analysis. Existing IDEs tend to illustrate the state of the art in tooling for one language at a time, and recent languages like Pony or Rust illustrate the state of the art in designing languages to make such analysis easy. For your specific example it seems easiest to just go with a pure functional language. Haskell compilers do reorder statements in fairly radical ways. I like the approach of starting from the set of all programs, and gradually refining the set to specific desires. There has been a minor tradition of research here, for example Dijkstra's Guarded Command Language and the notion of Stepwise Refinement. I tangentially used this imagery in http://akkartik.name/post/modularity http://akkartik.name/post/modularity.
- pezo1919 7y ago
  By tool I mean something more than a language. Something like a proof assistant, but more visual: it would show the different "views" (parts) of the already provided code, let the user to focus on just arbitrary parts, but at any time switch back to the whole picture. I don't know much about proof assistants but I did not see how someone can force the assistant to focus only on particular parts and save these parts for later time. There might be multiple holes in the implementation and I would like to study them sometimes together but sometimes separately.
  - akkartik 7y ago
    I understand it's something beyond a language. But surely it has to make some assumptions about the stack it relies on? If such a tool existed but required you to switch to a whole new language, would that be acceptable? What if you had to switch to a whole new programming model? What if you couldn't benefit from any of the software written by others in mainstream platforms? In any case, I think you'll enjoy hanging out at https://futureofcoding.org/slack-readme https://futureofcoding.org/slack-readme where people often chat about different parts of this (huge) open problem. I do.
asdftemp 7y ago
> My main idea is that as a programmer what I do is constantly reducing the set of all programs to a particular program which satisfies the specification. An alternate point of view is to start with the specification, interpreted as a generally nondeterministic program, and then refine it using logically sound optimizations to render it executable. This is roughly the approach of Fiat: http://adam.chlipala.net/papers/FiatSNAPL17/ http://adam.chlipala.net/papers/FiatSNAPL17/ They’ve used it to generate crypto primitives that are in use: http://adam.chlipala.net/papers/FiatCryptoSP19/ http://adam.chlipala.net/papers/FiatCryptoSP19/
- pezo1919 7y ago
  Seems interesting, thanks!
GistNoesis 7y ago
Something like Barliman?
- pezo1919 7y ago
  Yes, this is a good example of a "smart IDE", however I am looking for something more holistic.
lgas 7y ago
In addition to Agda and Coq (and Idris) you might be interested in djinn (https://hackage.haskell.org/package/djinn https://hackage.haskell.org/package/djinn) and ghc-justdoit (https://github.com/nomeata/ghc-justdoit https://github.com/nomeata/ghc-justdoit) for Haskell. The ghc-justdoit page lists some related work as well.
- pezo1919 7y ago
  I don't really know haskell but that seems interesting. Can you please explain 1. the potential gains you have with the packages above 2. the drawbacks of using these opposed to a Dependent Typed language? It would help a lot to me.
crb002 7y ago
Test Driven Development does this. Each test is a theorem about your code.
- pezo1919 7y ago
  Yes it is true, but you might accidentally skip cases which a proof assistant will tell you about. There is much information you can specify than later extract from the already given piece of code eg. with dependent types.
sankha93 7y ago
I really like F* . It is very close to OCaml in design but allows you to write proofs using a SMT solver or tactic based proofs when the SMT solver gives up. Instead of a proof theoretic language like Coq, the language feels closer to something we regularly program with and the F* compiler can output OCaml and C code. The proofs are erased from the final executable code so you still end up with a program that you would write without proofs. Microsoft Research's project Everest is using it to write a verified HTTPS stack. Edit: formatting
- pezo1919 7y ago
  Do you have an idea how to fit F* with Unity or just for a regular C# job? Is it a good idea?
mbrock 7y ago
Check out Rodin and Event-B for some inspiration. http://www.event-b.org http://www.event-b.org https://en.wikipedia.org/wiki/Rodin_tool https://en.wikipedia.org/wiki/Rodin_tool Here the inventor demonstrates making a simple bank account simulator with the stepwise refinement approach: https://www.youtube.com/watch?v=fSWZWXx5ixc https://www.youtube.com/watch?v=fSWZWXx5ixc
- pezo1919 7y ago
  Thank you! Seems interesting! Will check out.
kryptt 7y ago
Edwin Bradley coined the technique Type driven development... You can look for a bunch of videos about it on YouTube

I am a high-schooler and I understand dependent types. (I am not the person you are replying to, but I am the person who first mentioned typed holes.) In type theory, there are things called "terms" and "types." A term is something like `fun x -> x`, or `(1, 2)`, or `1 + 1`. In short, a term is basically an expression. Each term has a type. For example, `fun x -> x` might have the type `a -> a` and `(1, 2)` might have type `Nat * Nat`. If a term has a type, it "inhabits" the type. "x has type T" is written `x : T`. According to an idea called the Curry-Howard correspondence, types can encode logical statements such that terms that inhabit the type are its proofs. Therefore, by inhabiting a type, you are really proving a theorem. With dependent types, the term and type languages are the same language, so you can mix them together. In short, types are terms. Here are some types in Martin-Lof type theory: --------- () : Unit The unit type is a type with one inhabitant, (). It can be interpreted as the type of the empty tuple. In the Curry-Howard correspondence, the unit type corresponds with truth. x : A y : B -------------- (x, y) : A * B A * B, the product type of A and B, is the type of pairs. It is based on the Cartesian product operation: https://en.wikipedia.org/wiki/Cartesian_product https://en.wikipedia.org/wiki/Cartesian_product In the Curry-Howard correspondence, the product type corresponds with logical conjunction (and). By proving A and proving B, you can prove A * B (AKA A /\ B). x : Empty ---------------- elim-empty x : a The empty type is the type with no inhabitants. If you have an inhabitant of the empty type, you can eliminate it to derive anything. The empty type corresponds with falsity, and its elimination means that false implies anything. x : A -------------- Inl x : A + B x : B -------------- Inr x : A + B The sum type is the tagged union, meaning "this or that." The type A + B means that the Inl tag holds an A and the Inr tag holds a B. The sum type corresponds with logical disjunction (or). f : A -> B x : A ------------------- f(x) : B The exponential type, the type of functions, means logical implication. If you have f, a proof that A implies B, and x, a proof of A, you can prove B by doing f(x). With dependent types, the product and exponential types are generalized into the dependent sum (sigma) and the dependent product (pi) types respectively. With the dependent sum type, or sigma type `Σ (x : A) B(x)`, the second component in the type is actually a function of A (meaning that B : A -> Type). The dependent sum type generalizes the product type so that the type of the second element of the pair is actually dependent on the first element. In the Curry-Howard correspondence, the sigma type corresponds with existential quantification, "there exists" or "for some." To prove Σ (x : A) B(x), you must inhabit A (show that A exists) and B(x) (where B is a logical statement about x, the inhabitant of A). With the dependent product type, or pi type `Π (x : A) B(x)`, B is also a function of A that returns a type. The dependent product type generalizes the exponential type so that the codomain of the function, B(x), is dependent on the function's input, x. The dependent product type corresponds with universal quantification, "for all." To prove Π (x : A) B(x), you must prove B(x) for every possible x, where B(x) is a logical statement about x. Why the dependent product type generalizes the exponential type and the dependent sum type generalizes the product type seems confusing at first glance, but it really isn't: Σ for x = 1 to n, B(x) = B(1) + B(2) + ... B(n), and if B(x) is some constant C, Σ for x = 1 to n, C = n * C. The same rule applies to types, as multiplication (product) is just repeated addition (dependent sum of a constant). Π is like Σ, but for repeated multiplication instead of repeated addition. After all, exponentiation is just repeated multiplication. Another type that you should be aware of is the equality type, `x = y`. In vanilla Martin-Lof type theory, `x = y` is inhabited by `Refl` if `x` and `y` have the same normal form (reduce to the same simplest form). However, there is ongoing research in a field called Homotopy Type Theory, which redefines the equality type in various ways. Finally, types themselves form a hierarchy. With dependent types, the types themselves are first-class values, and they have their own types. However, `Type : Type` leads to Girard's paradox (similar to Russell's paradox). The solution is for each type to be in a "universe" so that `Type l : Type (l + 1)`, where `l` is the universe level. Read about Martin-Lof type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory https://en.wikipedia.org/wiki/Intuitionistic_type_theory