On Mon, 2007-03-12 at 17:19 -0400, Jacques Carette wrote: > [This is what I do in my day job. This might shed a little light as to > why I am so interested in Felix's support for 'axioms' !]
I wish I had a day job like that :) At present, Felix outputs a Why file every compilation. This contains signatures of all the functions, and seems to pass thru Why ok. (Why is Jean-Christophe Filliâtre's language for translating proof obligations to a wide range of theorem provers and proof assistants). I plan to output the axioms too, just haven't got around to it yet. There are a variety of next steps but the easiest seems to be to introduce theorems, and try to get Simplify or whatever to prove them via Why. The proof step is offline so doesn't impact compilation speed. The problem is there are numerous other things to do. I'm even scared to do any advocacy at the moment. I read LtU and people want feature X, Y and Z all of which Felix can do now, or could be modified to do. One good LtU article would probably draw 20 people to try it, 15 would be impressed .. but none would join the team or use it. Eg "Felix does high performance high volume context switching of fibres". Yeah, I have a test case that runs 500K trx/sec, 500K threads, no worries. Only when I tried launching many fthreads in a simple program it bogged down around 10K threads .. I have no idea why. I hate to make a claim that is proven wrong the first try. -- John Skaller <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net ------------------------------------------------------------------------- Take Surveys. Earn Cash. Influence the Future of IT Join SourceForge.net's Techsay panel and you'll get the chance to share your opinions on IT & business topics through brief surveys-and earn cash http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV _______________________________________________ Felix-language mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/felix-language
