4 ms·
Oh yeah, Ive known people who could do model checking giving up on Idris since it was too difficult. What's interesting about Noether is it builds up from simpl
by nickpsecurity 9y ago
Oh yeah, Ive known people who could do model checking giving up on Idris since it was too difficult. What's interesting about Noether is it builds up from simplest models of computation to single threaded to distributed. The lower levels are like state machines. One could do that in languages for contracts working up from brute-forceable automata toward more expressive stuff that takes more work.
Plus, I thought you'd enjoy the language presentation as extra benefit.
- willtim 9y agoAre we not confusing difficulty with familiarity? For me personally, as someone very familiar with FP, Idris was very approachable and easy to at least write simple proofs in.
- unboxed_type 9y agoI have nothing to say about the language (I gave up reading those cumbersome slides), but I am really amazed that you expect someone to like that presentation! :)