I love the Idris developments, but this thread gives a different perspective and gives interesting critiques.https://twitter.com/pressron/status/1115575346315841537 …
Sure, it's always good to look at these things from other people's perspectives. None of us have the definitive answers after all!
-
-
Demos of ideas, old or new, stick in people's minds. During a demo at SAC'19 this week, showing a proof language to verify C functions (Frama-C), an audience question was "is that specification precise enough to generate the C function" was influenced from Idris demos. 1/2
-
The question at SAC'19 was about the idea of generating implementation code from precise-enough specs. frama-c for generating correct imperative C code (?), Idris for generating correct functional code, etc. Implementations come and go, good ideas live on. 2/2
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.