Re: [isabelle] “Programming in Isabelle/HOL”



On 02/19/2014 07:43 PM, Makarius wrote:
>> On Wed, 19 Feb 2014, Yannick Duchêne (Hibou57) wrote:
>
>>> I will avoid posting it in other places (unfortunately, I already posted
>>> it on StackOverflow yesterday, in a comment).
>
> In the worst case you can delete notes on StackOverflow.
>
Please, could you do that, Yannick?
>
> I've looked through the notes for 5min.  Something in education must have
> gone utterly wrong if people are more familiar with WHILE, GOTO, poking
> around in memory than just plain and basic functional recursion.
>
Unfortunately, that is the state of the art in academic mathematics education:

* the example with WHILE and GOTO is a 1:1 copy from a _standard textbook
   on algorithms in computer algebra_
* students in mathematics learn thinking about computers via Java
    programming (I checked 7 universities in the area 2 years ago)

So a kind request to the list: who knows academic curricula which

(1) use a functional language as a _first introduction to programming_
     (and NOT as an additional choice later on)
/\(2) address students in _mathematics_, not only computer science
/\(3) include proving properties of programs as an essential part.

Please provide me with links to such courses; I'd collect them and publish it in the list !

(as a motivation for all who are convinced, that the next generation of textbooks on algorithmic mathematics should go beyond Isabelle/ML and rely on Isabelle/Isar or Coq --- and that education is a key for such changes)


PS: I know the introductory course of Tobias Nipkow at TUM based on
    http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/prog-prove.pdf




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.