me: "Hey, $young_local_hacker, you should learn #openscad!"
$young_local_hacker: But I already know openscad.
me: Then you should use it more!
$young_local_hacker: Well, the last thing I tried with it was implementing a neural network in it, but matrix handling is kind of weird in openscad.
This fucking kid will go places. <3
@phryk
#Homogeneous #coordinates, although seem weird at first, are, in fact, very elegant.
I'm also thinking about generation of #OpenSCAD #CSG models from #Coq specifications (just like e.g. #OCaml or #Scheme programs).
Can you think about a practical problem which would benefit from this approach?
@amiloradovsky Sorry, no clue – I'm pretty fresh to openSCAD and CAD in general.
I just have a bit of a home advantage because I already dabbled in POV-Ray, which is basically openSCAD for graphical stuff.
Wasn't Coq some proof generator? I remember sleeping through a talk on this a few years back… :D
@phryk
Yes, #Coq is a proof assistant (mostly proof checker, but some deterministic proof generation is also present).
The proofs may be seen as programs and the theorems — as their specifications/types. There are actual modules for extracting the programs in real world programming languages from the Coq programs.
What if we replace the (generated) programs with mechanical models or (digital) electronic circuitry? Seems feasible, and, in a sense, has been done already (#ACL2).
@phryk
The examples above are mostly about the controlling programs. But what if the #mechanics itself has dozens of movable parts, and it's #configuration #space is incomprehensible, not to speak about the #energy levels and stuff. So the #kinematics alone may be far from obvious, not to mention #dynamics.
First thing that comes to mind is the #gimbal #lock and similar situations, whose existence and (in)accessibility may be difficult to check, or at least tedious, error prone.
@phryk
Moreover, there may also be some unexpected #dynamic #regimes (e.g. #oscillations), which one might want to avoid or exploit.
Yet finding them all (i.e. exhaustive classification) and the optimal procedures to enter/avoid the states may also be not a trivial task.
Sure these issues in practice are (partially) solved by #simulations. But #simulation is more like #testing in #software development — (relatively) cheap & easy, but very inefficient with respect to the quality.
@amiloradovsky I'm afraid I'm just not qualified enough in that area. Tho this sounds a bit like deriving implementations from a set of constraints, which would be amazing.
I always wanted something where I can just specify a boat by a dozen or so variables and it'd model me a stable hull satisfying all constraints…
But that's for seasteading which I if at all I will only get around to in 2030 or something. :P
@phryk @amiloradovsky "deterministic" <- I wish.
Anyway, this seems like a reasonable idea. Synthesis in Coq is an area of active and fruitful research.
@phryk
This way one may check that a program doesn't access a memory outside the specified region, or a processor doesn't enter an unspecified state due to a peculiar sequence of instructions.
I suspect, this may also be used to prove things about, say, an assembly line, and make it more efficient by virtue of the static analysis.