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
>>> 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
* 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
PS: I know the introductory course of Tobias Nipkow at TUM based on
This archive was generated by a fusion of
Pipermail (Mailman edition) and