6 ms·

Im sure this is useful but these languages (proof langs, constraints, etc) are always so difficult to parse or read Adoption for these systems might be higher

Im sure this is useful but these languages (proof langs, constraints, etc) are always so difficult to parse or read Adoption for these systems might be higher if they had a more readable syntax (and bonus if they could transpile down to source code you can tweak) Also maybe I missed it on mobile, but I would love examples of the syntax and examples of application usage on the first page. Maybe this is useful to me! Who knows? That information should be easy to find

aidos 3y ago
I’ve played with minizinc in the past though we use scipopt now instead. The minizinc code looks pretty reasonable to me though. Specify your variables as ranges. Specify your constraints as math equations. Tell it what you’re looking to maximise / minimise. https://www.minizinc.org/doc-2.7.6/en/modelling.html#ex-cakes https://www.minizinc.org/doc-2.7.6/en/modelling.html#ex-cake...
- antegamisou 3y ago
  Judging from this particular example, it doesn't look a lot different than more established optimization software like CVXPY, no? https://www.cvxpy.org/examples/basic/linear_program.html https://www.cvxpy.org/examples/basic/linear_program.html
mirekrusin 3y ago
Yes exactly, we need typescript style solution to get best 80% of ocaml/haskell available to joes kind of thing.
- yakshaving_jgt 3y ago
  Do you not find this idea somewhat embarrassing? Why does everything need to look like JavaScript in order for Average Joe programmer to be able to read it?
  - mirekrusin 3y ago
    It absolutely doesn’t. But I can’t use OCaml or Coq at work. I can use typescript. I can use algebraic data types, well typed functional combinators, exhaustive switch statements (through linter) and other functional design patterns. I’d like to be able to use formal proofs. If it means dumbed down version that average joe can work with that can gain wider adoption - that’s much better situation to be in than not having anything at all. There must be more developers in similar situation.

aidos 3y ago

I’ve played with minizinc in the past though we use scipopt now instead. The minizinc code looks pretty reasonable to me though. Specify your variables as ranges. Specify your constraints as math equations. Tell it what you’re looking to maximise / minimise. https://www.minizinc.org/doc-2.7.6/en/modelling.html#ex-cakes https://www.minizinc.org/doc-2.7.6/en/modelling.html#ex-cake...

antegamisou 3y ago
Judging from this particular example, it doesn't look a lot different than more established optimization software like CVXPY, no? https://www.cvxpy.org/examples/basic/linear_program.html https://www.cvxpy.org/examples/basic/linear_program.html

mirekrusin 3y ago

Yes exactly, we need typescript style solution to get best 80% of ocaml/haskell available to joes kind of thing.

yakshaving_jgt 3y ago
Do you not find this idea somewhat embarrassing? Why does everything need to look like JavaScript in order for Average Joe programmer to be able to read it?
- mirekrusin 3y ago
  It absolutely doesn’t. But I can’t use OCaml or Coq at work. I can use typescript. I can use algebraic data types, well typed functional combinators, exhaustive switch statements (through linter) and other functional design patterns. I’d like to be able to use formal proofs. If it means dumbed down version that average joe can work with that can gain wider adoption - that’s much better situation to be in than not having anything at all. There must be more developers in similar situation.